@[reducible, inline]

abbrev Relation (α : Type u_1) (β : Type u_2) : Type (max u_2 u_1)

Equations

• Relation α β = Set (α × β)

def Relation.domain {α : Type u_1} {β : Type u_2} (r : Relation α β) : Set α

Equations

• r.domain = {a : α | ∃ (b : β), (a, b) ∈ r}

def Relation.range {α : Type u_1} {β : Type u_2} (r : Relation α β) : Set β

Equations

• r.range = {b : β | ∃ (a : α), (a, b) ∈ r}

@[simp]

theorem Relation.mem_domain_iff {α : Type u_1} {β : Type u_2} {r : Relation α β} {a : α} : a ∈ r.domain ↔ ∃ (b : β), (a, b) ∈ r

@[simp]

theorem Relation.mem_range_iff {α : Type u_1} {β : Type u_2} {r : Relation α β} {b : β} : b ∈ r.range ↔ ∃ (a : α), (a, b) ∈ r

theorem Relation.mem_domain_of {α : Type u_1} {β : Type u_2} {r : Relation α β} {a : α} {b : β} (h : (a, b) ∈ r) : a ∈ r.domain

theorem Relation.mem_range_of {α : Type u_1} {β : Type u_2} {r : Relation α β} {a : α} {b : β} (h : (a, b) ∈ r) : b ∈ r.range

@[simp]

theorem Relation.rel_subset_prod {α : Type u_1} {β : Type u_2} {r : Relation α β} : r ⊆ r.domain.prod r.range

theorem Relation.rel_nonempty_iff_domain_and_range_nonempty {α : Type u_1} {β : Type u_2} {r : Relation α β} : Set.Nonempty r ↔ r.domain.Nonempty ∧ r.range.Nonempty

theorem Relation.rel_nonempty_of_domain_nonempty {α : Type u_1} {β : Type u_2} {r : Relation α β} : r.domain.Nonempty → Set.Nonempty r

theorem Relation.rel_nonempty_of_range_nonempty {α : Type u_1} {β : Type u_2} {r : Relation α β} : r.range.Nonempty → Set.Nonempty r

def Relation.image {α : Type u_1} {β : Type u_2} (r : Relation α β) (x : Set α) : Set β

Equations

• r.image x = {b : β | ∃ (a : α), (a, b) ∈ r ∧ a ∈ x}

def Relation.preimage {α : Type u_1} {β : Type u_2} (r : Relation α β) (y : Set β) : Set α

Equations

• r.preimage y = {a : α | ∃ (b : β), (a, b) ∈ r ∧ b ∈ y}

@[simp]

theorem Relation.mem_image_iff {α : Type u_1} {β : Type u_2} {r : Relation α β} {b : β} {x : Set α} : b ∈ r.image x ↔ ∃ (a : α), (a, b) ∈ r ∧ a ∈ x

@[simp]

theorem Relation.mem_preimage_iff {α : Type u_1} {β : Type u_2} {r : Relation α β} {a : α} {y : Set β} : a ∈ r.preimage y ↔ ∃ (b : β), (a, b) ∈ r ∧ b ∈ y

@[simp]

theorem Relation.image_univ_range {α : Type u_1} {β : Type u_2} {r : Relation α β} : r.image Set.univ = r.range

@[simp]

theorem Relation.preimage_univ_domain {α : Type u_1} {β : Type u_2} {r : Relation α β} : r.preimage Set.univ = r.domain

@[simp]

theorem Relation.image_domain_range {α : Type u_1} {β : Type u_2} {r : Relation α β} : r.image r.domain = r.range

@[simp]

theorem Relation.preimage_range_domain {α : Type u_1} {β : Type u_2} {r : Relation α β} : r.preimage r.range = r.domain

@[simp]

theorem Relation.image_empty {α : Type u_1} {β : Type u_2} {r : Relation α β} : r.image ∅ = ∅

@[simp]

theorem Relation.preimage_empty {α : Type u_1} {β : Type u_2} {r : Relation α β} : r.preimage ∅ = ∅

@[simp]

theorem Relation.image_empty_rel {α : Type u_1} {β : Type u_2} {x : Set α} : ∅.image x = ∅

@[simp]

theorem Relation.preimage_empty_rel {α : Type u_1} {β : Type u_2} {y : Set β} : ∅.preimage y = ∅

@[simp]

theorem Relation.range_empty_rel {α : Type u_1} {β : Type u_2} : ∅.range = ∅

@[simp]

theorem Relation.domain_empty_rel {α : Type u_1} {β : Type u_2} : ∅.domain = ∅

@[simp]

theorem Relation.image_univ_rel {α : Type u_1} {β : Type u_2} {x : Set α} (h : x.Nonempty) : Relation.image Set.univ x = Set.univ

@[simp]

theorem Relation.preimage_univ_rel {α : Type u_1} {β : Type u_2} {y : Set β} (h : y.Nonempty) : Relation.preimage Set.univ y = Set.univ

@[simp]

theorem Relation.range_univ_rel {α : Type u_1} {β : Type u_2} [h : Nonempty α] : Relation.range Set.univ = Set.univ

@[simp]

theorem Relation.domain_univ_rel {α : Type u_1} {β : Type u_2} [h : Nonempty β] : Relation.domain Set.univ = Set.univ

theorem Relation.image_mono_left {α : Type u_1} {β : Type u_2} {r r' : Relation α β} {x : Set α} (h : r ⊆ r') : r.image x ⊆ r'.image x

theorem Relation.image_mono_right {α : Type u_1} {β : Type u_2} {r : Relation α β} {x x' : Set α} (h : x ⊆ x') : r.image x ⊆ r.image x'

theorem Relation.image_mono {α : Type u_1} {β : Type u_2} {r r' : Relation α β} {x x' : Set α} (h : r ⊆ r') (h' : x ⊆ x') : r.image x ⊆ r'.image x'

theorem Relation.preimage_mono_left {α : Type u_1} {β : Type u_2} {r r' : Relation α β} {y : Set β} (h : r ⊆ r') : r.preimage y ⊆ r'.preimage y

theorem Relation.preimage_mono_right {α : Type u_1} {β : Type u_2} {r : Relation α β} {y y' : Set β} (h : y ⊆ y') : r.preimage y ⊆ r.preimage y'

theorem Relation.preimage_mono {α : Type u_1} {β : Type u_2} {r r' : Relation α β} {y y' : Set β} (h : r ⊆ r') (h' : y ⊆ y') : r.preimage y ⊆ r'.preimage y'

theorem Relation.range_mono {α : Type u_1} {β : Type u_2} {r r' : Relation α β} (h : r ⊆ r') : r.range ⊆ r'.range

theorem Relation.domain_mono {α : Type u_1} {β : Type u_2} {r r' : Relation α β} (h : r ⊆ r') : r.domain ⊆ r'.domain

@[simp]

theorem Relation.image_subset_range {α : Type u_1} {β : Type u_2} {r : Relation α β} {x : Set α} : r.image x ⊆ r.range

@[simp]

theorem Relation.preimage_subset_domain {α : Type u_1} {β : Type u_2} {r : Relation α β} {y : Set β} : r.preimage y ⊆ r.domain

theorem Relation.image_of_domain_subset {α : Type u_1} {β : Type u_2} {r : Relation α β} {x : Set α} (h : r.domain ⊆ x) : r.image x = r.range

theorem Relation.preimage_of_range_subset {α : Type u_1} {β : Type u_2} {r : Relation α β} {y : Set β} (h : r.range ⊆ y) : r.preimage y = r.domain

def Relation.sect {α : Type u_1} {β : Type u_2} (r : Relation α β) (a : α) : Set β

Equations

• r.sect a = r.image {a}

@[simp]

theorem Relation.mem_sect_iff {α : Type u_1} {β : Type u_2} {r : Relation α β} {a : α} {b : β} : b ∈ r.sect a ↔ (a, b) ∈ r

theorem Relation.rel_subset_iff_sect_subset {α : Type u_1} {β : Type u_2} {r r' : Relation α β} : r ⊆ r' ↔ ∀ (a : α), r.sect a ⊆ r'.sect a

theorem Relation.sect_mono {α : Type u_1} {β : Type u_2} {r r' : Relation α β} {a : α} (h : r ⊆ r') : r.sect a ⊆ r'.sect a

theorem Relation.curry_eq_sect {α : Type u_1} {β : Type u_2} {r : Relation α β} : Function.curry r = r.sect

def Relation.inv {α : Type u_1} {β : Type u_2} (r : Relation α β) : Relation β α

Equations

• r.inv = {p : β × α | (p.snd, p.fst) ∈ r}

@[simp]

theorem Relation.mem_inv_iff {α : Type u_1} {β : Type u_2} {r : Relation α β} {a : α} {b : β} : (b, a) ∈ r.inv ↔ (a, b) ∈ r

@[simp]

theorem Relation.domain_inv {α : Type u_1} {β : Type u_2} {r : Relation α β} : r.inv.domain = r.range

@[simp]

theorem Relation.range_inv {α : Type u_1} {β : Type u_2} {r : Relation α β} : r.inv.range = r.domain

@[simp]

theorem Relation.image_inv {α : Type u_1} {β : Type u_2} {r : Relation α β} {y : Set β} : r.inv.image y = r.preimage y

@[simp]

theorem Relation.preimage_inv {α : Type u_1} {β : Type u_2} {r : Relation α β} {x : Set α} : r.inv.preimage x = r.image x

@[simp]

theorem Relation.inv_empty {α : Type u_1} {β : Type u_2} : ∅.inv = ∅

@[simp]

theorem Relation.inv_univ {α : Type u_1} {β : Type u_2} : Relation.inv Set.univ = Set.univ

@[simp]

theorem Relation.inv_inv {α : Type u_1} {β : Type u_2} {r : Relation α β} : r.inv.inv = r

theorem Relation.inv_monotone {α : Type u_1} {β : Type u_2} {r r' : Relation α β} (h : r ⊆ r') : r.inv ⊆ r'.inv

theorem Relation.inv_compl {α : Type u_1} {β : Type u_2} {r : Relation α β} : Relation.inv rᶜ = r.invᶜ

@[simp]

theorem Relation.sprod_domain {α : Type u_1} {β : Type u_2} {x : Set α} {y : Set β} (h : y.Nonempty) : Relation.domain (x.prod y) = x

@[simp]

theorem Relation.sprod_range {α : Type u_1} {β : Type u_2} {x : Set α} {y : Set β} (h : x.Nonempty) : Relation.range (x.prod y) = y

@[simp]

theorem Relation.sprod_image {α : Type u_1} {β : Type u_2} {a : α} {x x' : Set α} {y : Set β} (h : a ∈ x) (h' : a ∈ x') : Relation.image (x.prod y) x' = y

@[simp]

theorem Relation.sprod_preimage {α : Type u_1} {β : Type u_2} {b : β} {x : Set α} {y y' : Set β} (h : b ∈ y) (h' : b ∈ y') : Relation.preimage (x.prod y) y' = x

@[simp]

theorem Relation.sprod_inv {α : Type u_1} {β : Type u_2} {x : Set α} {y : Set β} : Relation.inv (x.prod y) = y.prod x

@[simp]

theorem Relation.sprod_sect {α : Type u_1} {β : Type u_2} {a : α} {x : Set α} {y : Set β} (h : a ∈ x) : Relation.sect (x.prod y) a = y

def Relation.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : Relation α β) (s : Relation γ α) : Relation γ β

Equations

• r.comp s = {x : γ × β | ∃ (a : α), (x.fst, a) ∈ s ∧ (a, x.snd) ∈ r}

@[simp]

theorem Relation.mem_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : Relation α β} {s : Relation γ α} {b : β} {c : γ} : (c, b) ∈ r.comp s ↔ ∃ (a : α), (c, a) ∈ s ∧ (a, b) ∈ r

theorem Relation.mem_comp_of {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : Relation α β} {s : Relation γ α} {a : α} {b : β} {c : γ} (h : (c, a) ∈ s) (h' : (a, b) ∈ r) : (c, b) ∈ r.comp s

@[simp]

theorem Relation.comp_empty {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : Relation α β} : r.comp ∅ = ∅

@[simp]

theorem Relation.empty_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Relation γ α} : ∅.comp s = ∅

@[simp]

theorem Relation.comp_univ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : Relation α β} : r.comp Set.univ = Set.univ.prod r.range

@[simp]

theorem Relation.univ_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Relation γ α} : Relation.comp Set.univ s = s.domain.prod Set.univ

@[simp]

theorem Relation.inv_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : Relation α β} {s : Relation γ α} : (r.comp s).inv = s.inv.comp r.inv

@[simp]

theorem Relation.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : Relation α β} {s : Relation γ α} {t : Relation δ γ} : r.comp (s.comp t) = (r.comp s).comp t

theorem Relation.range_comp_subset {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : Relation α β} {s : Relation γ α} : (r.comp s).range ⊆ r.range

theorem Relation.domain_comp_subset {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : Relation α β} {s : Relation γ α} : (r.comp s).domain ⊆ s.domain

theorem Relation.range_comp_eq_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : Relation α β} {s : Relation γ α} : (r.comp s).range = r.image s.range

theorem Relation.range_domain_eq_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : Relation α β} {s : Relation γ α} : (r.comp s).domain = s.preimage r.domain

theorem Relation.comp_mono_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r r' : Relation α β} {s : Relation γ α} (h : r ⊆ r') : r.comp s ⊆ r'.comp s

theorem Relation.comp_mono_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : Relation α β} {s s' : Relation γ α} (h : s ⊆ s') : r.comp s ⊆ r.comp s'

theorem Relation.comp_mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r r' : Relation α β} {s s' : Relation γ α} (h : r ⊆ r') (h' : s ⊆ s') : r.comp s ⊆ r'.comp s'

theorem Relation.subset_preimage_image_of_subset_domain {α : Type u_1} {β : Type u_2} {r : Relation α β} {x : Set α} (h : x ⊆ r.domain) : x ⊆ r.preimage (r.image x)

theorem Relation.subset_preimage_image_iff_subset_domain {α : Type u_1} {β : Type u_2} {r : Relation α β} {x : Set α} : x ⊆ r.preimage (r.image x) ↔ x ⊆ r.domain

theorem Relation.subset_image_preimage_of_subset_range {α : Type u_1} {β : Type u_2} {r : Relation α β} {y : Set β} (h : y ⊆ r.range) : y ⊆ r.image (r.preimage y)

theorem Relation.subset_image_preimage_iff_subset_range {α : Type u_1} {β : Type u_2} {r : Relation α β} {y : Set β} : y ⊆ r.image (r.preimage y) ↔ y ⊆ r.range

theorem Relation.sprod_comp {α : Type u_1} {β : Type u_2} {r : Relation α β} {x : Set α} {y : Set β} : Relation.comp (y.prod x) r = (r.preimage y).prod x

theorem Relation.comp_sprod {α : Type u_1} {β : Type u_2} {r : Relation α β} {x : Set α} {y : Set β} : r.comp (y.prod x) = y.prod (r.image x)

@[simp]

theorem Relation.image_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : Relation α β} {s : Relation γ α} {z : Set γ} : (r.comp s).image z = r.image (s.image z)

@[simp]

theorem Relation.preimage_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : Relation α β} {s : Relation γ α} {y : Set β} : (r.comp s).preimage y = s.preimage (r.preimage y)

theorem Relation.sprod_comp_sprod_empty_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {x x' : Set α} {y : Set β} {w : Set γ} (h1 : y.Nonempty) (h2 : w.Nonempty) : Relation.comp (x.prod y) (w.prod x') = ∅ ↔ x ∩ x' = ∅

theorem Relation.sprod_comp_sprod_eq_sprod_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {x x' : Set α} {y : Set β} {w : Set γ} (h1 : y.Nonempty) (h2 : w.Nonempty) : Relation.comp (x.prod y) (w.prod x') = w.prod y ↔ x ∩ x' ≠ ∅

def Relation.diag {α : Type u_1} : Relation α α

Equations

• Relation.diag = {x : α × α | x.fst = x.snd}

@[simp]

theorem Relation.mem_diag_iff {α : Type u_1} {a a' : α} : (a, a') ∈ Relation.diag ↔ a = a'

@[simp]

theorem Relation.image_diag {α : Type u_1} {x : Set α} : Relation.diag.image x = x

@[simp]

theorem Relation.preimage_diag {α : Type u_1} {x : Set α} : Relation.diag.preimage x = x

@[simp]

theorem Relation.range_diag {α : Type u_1} : Relation.diag.range = Set.univ

@[simp]

theorem Relation.domain_diag {α : Type u_1} : Relation.diag.domain = Set.univ

@[simp]

theorem Relation.inv_diag {α : Type u_1} : Relation.diag.inv = Relation.diag

@[simp]

theorem Relation.diag_comp {α : Type u_1} {β : Type u_2} {r : Relation α β} : Relation.diag.comp r = r

@[simp]

theorem Relation.comp_diag {α : Type u_1} {β : Type u_2} {r : Relation α β} : r.comp Relation.diag = r

theorem Relation.comp_compl_inv_subset_diag_compl {α : Type u_1} {β : Type u_2} {r : Relation α β} : r.comp r.invᶜ ⊆ Relation.diagᶜ

theorem Relation.compl_inv_comp_subset_diag_compl {α : Type u_1} {β : Type u_2} {r : Relation α β} : Relation.comp r.invᶜ r ⊆ Relation.diagᶜ

theorem Relation.comp_compl_inv_comp_iff_prod {α : Type u_1} {β : Type u_2} {r : Relation α β} : r.comp (Relation.comp r.invᶜ r) = ∅ ↔ r = r.domain.prod r.range

def Relation.Functional {α : Type u_1} {β : Type u_2} (r : Relation α β) : Prop

Equations

• r.Functional = ∀ (x : α), ∃! y : β, (x, y) ∈ r

def Relation.graph {α : Type u_1} {β : Type u_2} (f : α → β) : Relation α β

Equations

• Relation.graph f = {x : α × β | x.snd = f x.fst}

@[simp]

theorem Relation.mem_graph_iff {α : Type u_1} {β : Type u_2} {a : α} {b : β} {f : α → β} : (a, b) ∈ Relation.graph f ↔ b = f a

@[simp]

theorem Relation.mem_graph {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} : (a, f a) ∈ Relation.graph f

@[simp]

theorem Relation.graph_functional {α : Type u_1} {β : Type u_2} {f : α → β} : (Relation.graph f).Functional

@[simp]

theorem Relation.functional_iff_graph {α : Type u_1} {β : Type u_2} {r : Relation α β} : r.Functional ↔ ∃ (f : α → β), r = Relation.graph f

@[simp]

theorem Relation.graph_section {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} : (Relation.graph f).sect a = {f a}

theorem Relation.diag_graph_id {α : Type u_1} : Relation.diag = Relation.graph id

theorem Relation.diag_functional {α : Type u_1} : Relation.diag.Functional

theorem Relation.graph_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : γ → α} : Relation.graph (f ∘ g) = (Relation.graph f).comp (Relation.graph g)

theorem Relation.functional_comp_of_functional {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : Relation α β} {s : Relation γ α} (h : r.Functional) (h' : s.Functional) : (r.comp s).Functional

@[simp]

theorem Relation.domain_graph {α : Type u_1} {β : Type u_2} {f : α → β} : (Relation.graph f).domain = Set.univ

theorem Relation.domain_functional {α : Type u_1} {β : Type u_2} {r : Relation α β} (h : r.Functional) : r.domain = Set.univ

theorem Relation.functional_iff_preimage_image {α : Type u_1} {β : Type u_2} {r : Relation α β} : r.Functional ↔ (∀ (y : Set β), r.image (r.preimage y) ⊆ y) ∧ r.domain = Set.univ

def Relation.inverse_image {α : Type u_1} {γ : Type u_5} (r : Relation α α) (f : γ → α) : Relation γ γ

Equations

• r.inverse_image f (x_1, y) = r (f x_1, f y)

@[simp]

theorem Relation.mem_inverse_image_iff {α : Type u_1} {γ : Type u_3} {r : Relation α α} {f : γ → α} {c c' : γ} : (c, c') ∈ r.inverse_image f ↔ (f c, f c') ∈ r

def Relation.restrict {α : Type u_1} (r : Relation α α) (x : Set α) : Relation ↥x ↥x

Equations

• r.restrict x (a, b) = r (a.val, b.val)

@[simp]

theorem Relation.mem_restrict_iff {α : Type u_1} {r : Relation α α} {x : Set α} {a a' : ↥x} : (a, a') ∈ r.restrict x ↔ (a.val, a'.val) ∈ r

theorem Relation.restrict_inverse_image {α : Type u_1} {r : Relation α α} {x : Set α} : r.restrict x = r.inverse_image Subtype.val

theorem Relation.injection_restrict_compatible {α : Type u_1} {r : Relation α α} {x : Set α} (a a' : ↥x) (h : (a, a') ∈ r.restrict x) : (a.val, a'.val) ∈ r

def Relation.prod_rel {α : Type u_1} {β : Type u_2} (r : Relation α α) (s : Relation β β) : Relation (α × β) (α × β)

Equations

• r.prod_rel s ((a, b), a', b') = ((a, a') ∈ r ∧ (b, b') ∈ s)

@[simp]

theorem Relation.mem_prod_rel_iff {α : Type u_1} {β : Type u_2} {r : Relation α α} {s : Relation β β} {a a' : α} {b b' : β} : ((a, b), a', b') ∈ r.prod_rel s ↔ (a, a') ∈ r ∧ (b, b') ∈ s