structure Rel.Injective {α : Type u_1} {β : Type u_2} (r : Rel α β) : Prop

• injective : ∀ ⦃x₁ x₂ : α⦄ ⦃y : β⦄, r x₁ y → r x₂ y → x₁ = x₂

theorem Rel.injective_iff {α : Type u_1} {β : Type u_2} (r : Rel α β) : r.Injective ↔ ∀ ⦃x₁ x₂ : α⦄ ⦃y : β⦄, r x₁ y → r x₂ y → x₁ = x₂

structure Rel.Coinjective {α : Type u_1} {β : Type u_2} (r : Rel α β) : Prop

• coinjective : ∀ ⦃y₁ y₂ : β⦄ ⦃x : α⦄, r x y₁ → r x y₂ → y₁ = y₂

theorem Rel.coinjective_iff {α : Type u_1} {β : Type u_2} (r : Rel α β) : r.Coinjective ↔ ∀ ⦃y₁ y₂ : β⦄ ⦃x : α⦄, r x y₁ → r x y₂ → y₁ = y₂

structure Rel.Surjective {α : Type u_1} {β : Type u_2} (r : Rel α β) : Prop

• surjective : ∀ (y : β), ∃ (x : α), r x y

theorem Rel.surjective_iff {α : Type u_1} {β : Type u_2} (r : Rel α β) : r.Surjective ↔ ∀ (y : β), ∃ (x : α), r x y

structure Rel.Cosurjective {α : Type u_1} {β : Type u_2} (r : Rel α β) : Prop

• cosurjective : ∀ (x : α), ∃ (y : β), r x y

theorem Rel.cosurjective_iff {α : Type u_1} {β : Type u_2} (r : Rel α β) : r.Cosurjective ↔ ∀ (x : α), ∃ (y : β), r x y

structure Rel.Functional {α : Type u_1} {β : Type u_2} (r : Rel α β) extends r.Coinjective, r.Cosurjective : Prop

• coinjective : ∀ ⦃y₁ y₂ : β⦄ ⦃x : α⦄, r x y₁ → r x y₂ → y₁ = y₂
• cosurjective : ∀ (x : α), ∃ (y : β), r x y

theorem Rel.functional_iff {α : Type u_1} {β : Type u_2} (r : Rel α β) : r.Functional ↔ r.Coinjective ∧ r.Cosurjective

structure Rel.Cofunctional {α : Type u_1} {β : Type u_2} (r : Rel α β) extends r.Injective, r.Surjective : Prop

• injective : ∀ ⦃x₁ x₂ : α⦄ ⦃y : β⦄, r x₁ y → r x₂ y → x₁ = x₂
• surjective : ∀ (y : β), ∃ (x : α), r x y

theorem Rel.cofunctional_iff {α : Type u_1} {β : Type u_2} (r : Rel α β) : r.Cofunctional ↔ r.Injective ∧ r.Surjective

structure Rel.OneOne {α : Type u_1} {β : Type u_2} (r : Rel α β) extends r.Injective, r.Coinjective : Prop

• injective : ∀ ⦃x₁ x₂ : α⦄ ⦃y : β⦄, r x₁ y → r x₂ y → x₁ = x₂
• coinjective : ∀ ⦃y₁ y₂ : β⦄ ⦃x : α⦄, r x y₁ → r x y₂ → y₁ = y₂

theorem Rel.oneOne_iff {α : Type u_1} {β : Type u_2} (r : Rel α β) : r.OneOne ↔ r.Injective ∧ r.Coinjective

structure Rel.Bijective {α : Type u_1} {β : Type u_2} (r : Rel α β) extends r.Functional, r.Cofunctional : Prop

• coinjective : ∀ ⦃y₁ y₂ : β⦄ ⦃x : α⦄, r x y₁ → r x y₂ → y₁ = y₂
• cosurjective : ∀ (x : α), ∃ (y : β), r x y
• injective : ∀ ⦃x₁ x₂ : α⦄ ⦃y : β⦄, r x₁ y → r x₂ y → x₁ = x₂
• surjective : ∀ (y : β), ∃ (x : α), r x y

theorem Rel.bijective_iff {α : Type u_1} {β : Type u_2} (r : Rel α β) : r.Bijective ↔ r.Functional ∧ r.Cofunctional

structure Rel.CodomEqDom {α : Type u_1} (r : Rel α α) : Prop

• codom_eq_dom : r.codom = r.dom

theorem Rel.codomEqDom_iff {α : Type u_1} (r : Rel α α) : r.CodomEqDom ↔ r.codom = r.dom

structure Rel.Permutative {α : Type u_1} (r : Rel α α) extends r.OneOne, r.CodomEqDom : Prop

• injective : ∀ ⦃x₁ x₂ y : α⦄, r x₁ y → r x₂ y → x₁ = x₂
• coinjective : ∀ ⦃y₁ y₂ x : α⦄, r x y₁ → r x y₂ → y₁ = y₂
• codom_eq_dom : r.codom = r.dom

theorem Rel.permutative_iff {α : Type u_1} (r : Rel α α) : r.Permutative ↔ r.OneOne ∧ r.CodomEqDom

theorem Rel.CodomEqDom.dom_union_codom {α : Type u_1} {r : Rel α α} (h : r.CodomEqDom) : r.dom ∪ r.codom = r.dom

theorem Rel.CodomEqDom.mem_dom {α : Type u_1} {r : Rel α α} (h : r.CodomEqDom) {x y : α} (hxy : r x y) : y ∈ r.dom

theorem Rel.CodomEqDom.mem_codom {α : Type u_1} {r : Rel α α} (h : r.CodomEqDom) {x y : α} (hxy : r x y) : x ∈ r.codom

theorem Rel.codomEqDom_iff' {α : Type u_1} (r : Rel α α) : r.CodomEqDom ↔ (∀ (x y : α), r x y → ∃ (z : α), r y z) ∧ ∀ (x y : α), r x y → ∃ (z : α), r z x

An elementary description of the property CodomEqDom.

theorem Rel.OneOne.inv {α : Type u_1} {β : Type u_2} {r : Rel α β} (h : r.OneOne) : r.inv.OneOne

@[simp]

theorem Rel.inv_apply {α : Type u_1} {β : Type u_2} {r : Rel α β} {x : α} {y : β} : r.inv y x ↔ r x y

theorem Rel.inv_injective {α : Type u_1} {β : Type u_2} : Function.Injective Rel.inv

@[simp]

theorem Rel.inv_inj {α : Type u_1} {β : Type u_2} {r s : Rel α β} : r.inv = s.inv ↔ r = s

@[simp]

theorem Rel.inv_injective_iff {α : Type u_1} {β : Type u_2} {r : Rel α β} : r.inv.Injective ↔ r.Coinjective

@[simp]

theorem Rel.inv_coinjective_iff {α : Type u_1} {β : Type u_2} {r : Rel α β} : r.inv.Coinjective ↔ r.Injective

@[simp]

theorem Rel.inv_surjective_iff {α : Type u_1} {β : Type u_2} {r : Rel α β} : r.inv.Surjective ↔ r.Cosurjective

@[simp]

theorem Rel.inv_cosurjective_iff {α : Type u_1} {β : Type u_2} {r : Rel α β} : r.inv.Cosurjective ↔ r.Surjective

@[simp]

theorem Rel.inv_functional_iff {α : Type u_1} {β : Type u_2} {r : Rel α β} : r.inv.Functional ↔ r.Cofunctional

@[simp]

theorem Rel.inv_cofunctional_iff {α : Type u_1} {β : Type u_2} {r : Rel α β} : r.inv.Cofunctional ↔ r.Functional

@[simp]

theorem Rel.inv_dom {α : Type u_1} {β : Type u_2} {r : Rel α β} : r.inv.dom = r.codom

@[simp]

theorem Rel.inv_codom {α : Type u_1} {β : Type u_2} {r : Rel α β} : r.inv.codom = r.dom

@[simp]

theorem Rel.inv_image {α : Type u_1} {β : Type u_2} {r : Rel α β} {s : Set β} : r.inv.image s = r.preimage s

@[simp]

theorem Rel.inv_preimage {α : Type u_1} {β : Type u_2} {r : Rel α β} {s : Set α} : r.inv.preimage s = r.image s

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

theorem Rel.Injective.image_injective {α : Type u_1} {β : Type u_2} {r : Rel α β} (h : r.Injective) {s t : Set α} (hs : s ⊆ r.dom) (ht : t ⊆ r.dom) (hst : r.image s = r.image t) : s = t

theorem Rel.subset_image_of_preimage_subset {α : Type u_1} {β : Type u_2} {r : Rel α β} {s : Set β} (hs : s ⊆ r.codom) (t : Set α) : r.preimage s ⊆ t → s ⊆ r.image t

theorem Rel.Injective.preimage_subset_of_subset_image {α : Type u_1} {β : Type u_2} {r : Rel α β} (h : r.Injective) (s : Set β) (t : Set α) : s ⊆ r.image t → r.preimage s ⊆ t

theorem Rel.Injective.preimage_subset_iff_subset_image {α : Type u_1} {β : Type u_2} {r : Rel α β} (h : r.Injective) (s : Set β) (hs : s ⊆ r.codom) (t : Set α) : r.preimage s ⊆ t ↔ s ⊆ r.image t

theorem Rel.OneOne.preimage_eq_iff_image_eq {α : Type u_1} {β : Type u_2} {r : Rel α β} (h : r.OneOne) {s : Set β} (hs : s ⊆ r.codom) {t : Set α} (ht : t ⊆ r.dom) : r.preimage s = t ↔ r.image t = s

theorem Rel.CodomEqDom.inv {α : Type u_1} {r : Rel α α} (h : r.CodomEqDom) : r.inv.CodomEqDom

theorem Rel.Permutative.inv {α : Type u_1} {r : Rel α α} (h : r.Permutative) : r.inv.Permutative

theorem Rel.Permutative.inv_dom {α : Type u_1} {r : Rel α α} (h : r.Permutative) : r.inv.dom = r.dom

theorem Rel.Injective.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : Rel α β} {s : Rel β γ} (hr : r.Injective) (hs : s.Injective) : (r.comp s).Injective

theorem Rel.Coinjective.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : Rel α β} {s : Rel β γ} (hr : r.Coinjective) (hs : s.Coinjective) : (r.comp s).Coinjective

theorem Rel.Injective.mono {α : Type u_1} {β : Type u_2} {r s : Rel α β} (hs : s.Injective) (h : r ≤ s) : r.Injective

theorem Rel.Coinjective.mono {α : Type u_1} {β : Type u_2} {r s : Rel α β} (hs : s.Coinjective) (h : r ≤ s) : r.Coinjective

theorem Rel.OneOne.mono {α : Type u_1} {β : Type u_2} {r s : Rel α β} (hs : s.OneOne) (h : r ≤ s) : r.OneOne

def Rel.graph' {α : Type u_1} {β : Type u_2} (r : Rel α β) : Set (α × β)

An alternative spelling of Rel.graph that is useful for proving inequalities of cardinals.

Equations

• r.graph' = Function.uncurry r

theorem Rel.le_of_graph'_subset {α : Type u_1} {β : Type u_2} {r s : Rel α β} (h : r.graph' ⊆ s.graph') : r ≤ s

theorem Rel.graph'_subset_of_le {α : Type u_1} {β : Type u_2} {r s : Rel α β} (h : r ≤ s) : r.graph' ⊆ s.graph'

theorem Rel.graph'_subset_iff {α : Type u_1} {β : Type u_2} {r s : Rel α β} : r.graph' ⊆ s.graph' ↔ r ≤ s

theorem Rel.graph'_injective {α : Type u_1} {β : Type u_2} : Function.Injective Rel.graph'

@[simp]

theorem Rel.image_dom {α : Type u_1} {β : Type u_2} {r : Rel α β} : r.image r.dom = r.codom

@[simp]

theorem Rel.preimage_codom {α : Type u_1} {β : Type u_2} {r : Rel α β} : r.preimage r.codom = r.dom

theorem Rel.preimage_subset_dom {α : Type u_1} {β : Type u_2} (r : Rel α β) (t : Set β) : r.preimage t ⊆ r.dom

theorem Rel.image_subset_codom {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set α) : r.image s ⊆ r.codom

theorem Rel.image_empty_of_disjoint_dom {α : Type u_1} {β : Type u_2} {r : Rel α β} {s : Set α} (h : Disjoint r.dom s) : r.image s = ∅

theorem Rel.image_eq_of_inter_eq {α : Type u_1} {β : Type u_2} {r : Rel α β} {s t : Set α} (h : s ∩ r.dom = t ∩ r.dom) : r.image s = r.image t

theorem Rel.Injective.image_diff {α : Type u_1} {β : Type u_2} {r : Rel α β} (h : r.Injective) (s t : Set α) : r.image (s \ t) = r.image s \ r.image t

theorem Rel.Injective.image_symmDiff {α : Type u_1} {β : Type u_2} {r : Rel α β} (h : r.Injective) (s t : Set α) : r.image (symmDiff s t) = symmDiff (r.image s) (r.image t)

theorem Rel.image_eq_of_le_of_le {α : Type u_1} {β : Type u_2} {r s : Rel α β} (h : r ≤ s) {t : Set α} (ht : ∀ x ∈ t, s x ≤ r x) : r.image t = s.image t

@[simp]

theorem Rel.sup_inv {α : Type u_1} {β : Type u_2} {r s : Rel α β} : (r ⊔ s).inv = r.inv ⊔ s.inv

theorem Rel.sup_apply {α : Type u_1} {β : Type u_2} {r s : Rel α β} {x : α} {y : β} : (r ⊔ s) x y ↔ r x y ∨ s x y

@[simp]

theorem Rel.sup_dom {α : Type u_1} {β : Type u_2} {r s : Rel α β} : (r ⊔ s).dom = r.dom ∪ s.dom

@[simp]

theorem Rel.sup_codom {α : Type u_1} {β : Type u_2} {r s : Rel α β} : (r ⊔ s).codom = r.codom ∪ s.codom

@[simp]

theorem Rel.sup_image {α : Type u_1} {β : Type u_2} {r s : Rel α β} (t : Set α) : (r ⊔ s).image t = r.image t ∪ s.image t

theorem Rel.sup_injective {α : Type u_1} {β : Type u_2} {r s : Rel α β} (hr : r.Injective) (hs : s.Injective) (h : Disjoint r.codom s.codom) : (r ⊔ s).Injective

theorem Rel.sup_coinjective {α : Type u_1} {β : Type u_2} {r s : Rel α β} (hr : r.Coinjective) (hs : s.Coinjective) (h : Disjoint r.dom s.dom) : (r ⊔ s).Coinjective

theorem Rel.sup_oneOne {α : Type u_1} {β : Type u_2} {r s : Rel α β} (hr : r.OneOne) (hs : s.OneOne) (h₁ : Disjoint r.dom s.dom) (h₂ : Disjoint r.codom s.codom) : (r ⊔ s).OneOne

theorem Rel.sup_codomEqDom {α : Type u_1} {r s : Rel α α} (hr : r.CodomEqDom) (hs : s.CodomEqDom) : (r ⊔ s).CodomEqDom

theorem Rel.sup_permutative {α : Type u_1} {r s : Rel α α} (hr : r.Permutative) (hs : s.Permutative) (h : Disjoint r.dom s.dom) : (r ⊔ s).Permutative

@[simp]

theorem Rel.inf_inv {α : Type u_1} {β : Type u_2} {r s : Rel α β} : (r ⊓ s).inv = r.inv ⊓ s.inv

theorem Rel.inf_apply {α : Type u_1} {β : Type u_2} {r s : Rel α β} {x : α} {y : β} : (r ⊓ s) x y ↔ r x y ∧ s x y

theorem Rel.inf_dom {α : Type u_1} {β : Type u_2} {r s : Rel α β} : (r ⊓ s).dom ⊆ r.dom ∩ s.dom

theorem Rel.inf_codom {α : Type u_1} {β : Type u_2} {r s : Rel α β} : (r ⊓ s).codom ⊆ r.codom ∩ s.codom

@[simp]

theorem Rel.inv_le_inv_iff {α : Type u_1} {β : Type u_2} {r s : Rel α β} : r.inv ≤ s.inv ↔ r ≤ s

@[simp]

theorem Rel.iSup_apply_iff {α : Type u_2} {β : Type u_3} {T : Type u_1} {r : T → Rel α β} (x : α) (y : β) : (⨆ (t : T), r t) x y ↔ ∃ (t : T), r t x y

@[simp]

theorem Rel.biSup_apply_iff {α : Type u_2} {β : Type u_3} {T : Type u_1} {r : T → Rel α β} {s : Set T} (x : α) (y : β) : (⨆ t ∈ s, r t) x y ↔ ∃ t ∈ s, r t x y

theorem Rel.iSup_dom {α : Type u_2} {β : Type u_3} {T : Type u_1} (r : T → Rel α β) : (⨆ (t : T), r t).dom = ⋃ (t : T), (r t).dom

theorem Rel.biSup_dom {α : Type u_2} {β : Type u_3} {T : Type u_1} (r : T → Rel α β) (s : Set T) : (⨆ t ∈ s, r t).dom = ⋃ t ∈ s, (r t).dom

theorem Rel.isChain_inv {α : Type u_2} {β : Type u_3} {T : Type u_1} {r : T → Rel α β} (h : IsChain (fun (x1 x2 : Rel α β) => x1 ≤ x2) (Set.range r)) : IsChain (fun (x1 x2 : Rel β α) => x1 ≤ x2) (Set.range fun (t : T) => (r t).inv)

theorem Rel.iSup_inv {α : Type u_2} {β : Type u_3} {T : Type u_1} {r : T → Rel α β} : ⨆ (t : T), (r t).inv = (⨆ (t : T), r t).inv

theorem Rel.iSup_injective_of_isChain {α : Type u_2} {β : Type u_3} {T : Type u_1} {r : T → Rel α β} (h₁ : ∀ (t : T), (r t).Injective) (h₂ : IsChain (fun (x1 x2 : Rel α β) => x1 ≤ x2) (Set.range r)) : (⨆ (t : T), r t).Injective

theorem Rel.iSup_coinjective_of_isChain {α : Type u_2} {β : Type u_3} {T : Type u_1} {r : T → Rel α β} (h₁ : ∀ (t : T), (r t).Coinjective) (h₂ : IsChain (fun (x1 x2 : Rel α β) => x1 ≤ x2) (Set.range r)) : (⨆ (t : T), r t).Coinjective

theorem Rel.iSup_codomEqDom_of_isChain {α : Type u_2} {T : Type u_1} {r : T → Rel α α} (h : ∀ (t : T), (r t).CodomEqDom) : (⨆ (t : T), r t).CodomEqDom

theorem Rel.iSup_oneOne_of_isChain {α : Type u_2} {β : Type u_3} {T : Type u_1} {r : T → Rel α β} (h₁ : ∀ (t : T), (r t).OneOne) (h₂ : IsChain (fun (x1 x2 : Rel α β) => x1 ≤ x2) (Set.range r)) : (⨆ (t : T), r t).OneOne

theorem Rel.iSup_permutative_of_isChain {α : Type u_2} {T : Type u_1} {r : T → Rel α α} (h₁ : ∀ (t : T), (r t).Permutative) (h₂ : IsChain (fun (x1 x2 : Rel α α) => x1 ≤ x2) (Set.range r)) : (⨆ (t : T), r t).Permutative

theorem Rel.biSup_permutative_of_isChain {α : Type u_2} {T : Type u_1} {r : T → Rel α α} {s : Set T} (h₁ : ∀ t ∈ s, (r t).Permutative) (h₂ : IsChain (fun (x1 x2 : Rel α α) => x1 ≤ x2) (r '' s)) : (⨆ t ∈ s, r t).Permutative

noncomputable def Rel.toFunction {α : Type u_1} {β : Type u_2} (r : Rel α β) (hr : r.Functional) : α → β

Equations

• r.toFunction hr a = ⋯.choose

theorem Rel.toFunction_rel {α : Type u_1} {β : Type u_2} (r : Rel α β) (hr : r.Functional) (a : α) : r a (r.toFunction hr a)

theorem Rel.toFunction_eq_iff {α : Type u_1} {β : Type u_2} (r : Rel α β) (hr : r.Functional) (a : α) (b : β) : r.toFunction hr a = b ↔ r a b

noncomputable def Rel.toEquiv {α : Type u_1} {β : Type u_2} (r : Rel α β) (hr : r.Bijective) : α ≃ β

Equations

• r.toEquiv hr = { toFun := r.toFunction ⋯, invFun := r.inv.toFunction ⋯, left_inv := ⋯, right_inv := ⋯ }

theorem Rel.toEquiv_rel {α : Type u_1} {β : Type u_2} (r : Rel α β) (hr : r.Bijective) (a : α) : r a ((r.toEquiv hr) a)

theorem Rel.toEquiv_eq_iff {α : Type u_1} {β : Type u_2} (r : Rel α β) (hr : r.Bijective) (a : α) (b : β) : (r.toEquiv hr) a = b ↔ r a b

theorem Rel.toFunction_image {α : Type u_1} {β : Type u_2} (r : Rel α β) (hr : r.Functional) (s : Set α) : r.toFunction hr '' s = r.image s

theorem Rel.toEquiv_image {α : Type u_1} {β : Type u_2} (r : Rel α β) (hr : r.Bijective) (s : Set α) : ⇑(r.toEquiv hr) '' s = r.image s