@[reducible, inline]

abbrev Relation.IsEquivalence {α : Type u_1} (r : Relation α α) : Prop

Equations

• r.IsEquivalence = Equivalence fun (a b : α) => (a, b) ∈ r

theorem Relation.equiv_refl {α : Type u_1} {r : Relation α α} [inst : r.IsEquivalence] {a : α} : (a, a) ∈ r

theorem Relation.equiv_symm {α : Type u_1} {r : Relation α α} [inst : r.IsEquivalence] {a b : α} (h : (a, b) ∈ r) : (b, a) ∈ r

theorem Relation.equiv_trans {α : Type u_1} {r : Relation α α} [inst : r.IsEquivalence] {a b c : α} (h : (a, b) ∈ r) (h' : (b, c) ∈ r) : (a, c) ∈ r

instance Relation.instIsEquivalenceUnivProd {α : Type u_1} : Relation.IsEquivalence Set.univ

Equations

• ⋯ = ⋯

instance Relation.instIsEquivalenceDiag {α : Type u_1} : Relation.diag.IsEquivalence

Equations

• ⋯ = ⋯

instance Relation.instIsEquivalenceInverse_image {α : Type u_1} {γ : Type u_2} {r : Relation α α} {f : γ → α} [inst : r.IsEquivalence] : (r.inverse_image f).IsEquivalence

Equations

• ⋯ = ⋯

instance Relation.instIsEquivalenceSubtypeMemSetRestrict {α : Type u_1} {r : Relation α α} {x : Set α} [inst : r.IsEquivalence] : (r.restrict x).IsEquivalence

Equations

• ⋯ = ⋯

instance Relation.instIsEquivalenceIInterProd {α : Type u_1} {ι : Type u_3} {r : ι → Relation α α} [inst : ∀ (x : ι), (r x).IsEquivalence] : Relation.IsEquivalence (⋂ i : ι, r i)

Equations

• ⋯ = ⋯

theorem Relation.isEquivalence_in_set_or_compl {α : Type u_1} (x : Set α) : Relation.IsEquivalence fun (x_1 : α × α) => match x_1 with | (a, b) => a ∈ x ↔ b ∈ x

theorem Relation.isEquivalence_iff {α : Type u_1} {r : Relation α α} : r.IsEquivalence ↔ r.domain = Set.univ ∧ r.inv = r ∧ r.comp r = r

theorem Relation.isEquivalence_iff' {α : Type u_1} {r : Relation α α} : r.IsEquivalence ↔ r.comp (r.inv.comp r) = r ∧ Relation.diag ⊆ r

theorem Relation.isEquivalence_comp_of_comp_eq_left {α : Type u_1} {r : Relation α α} (h : r.domain = Set.univ) (h' : r.comp (r.inv.comp r) = r) : (r.inv.comp r).IsEquivalence

theorem Relation.isEquivalence_comp_of_comp_eq_right {α : Type u_1} {r : Relation α α} (h : r.range = Set.univ) (h' : r.comp (r.inv.comp r) = r) : (r.comp r.inv).IsEquivalence

theorem Relation.IsEquivalence.comp_right {α : Type u_3} {r : Relation α α} [inst : r.IsEquivalence] {s : Relation α α} (h : s ⊆ r) (h' : s.domain = Set.univ) : r.comp s = r

theorem Relation.IsEquivalence.comp_left {α : Type u_3} {r : Relation α α} [inst : r.IsEquivalence] {s : Relation α α} (h : s ⊆ r) (h' : s.range = Set.univ) : s.comp r = r

theorem Relation.IsEquivalence.inter_comp_commute {α : Type u_3} {r : Relation α α} [inst : r.IsEquivalence] {s t : Relation α α} (h : s ⊆ r) : (r ∩ t).comp s = r ∩ t.comp s

theorem Relation.IsEquivalence.comp_inter {α : Type u_3} {r : Relation α α} [inst : r.IsEquivalence] {s t : Relation α α} (h : s ⊆ r) : s.comp (r ∩ t) = r ∩ s.comp t

theorem Relation.IsEquivalence.comp_isEquivalence_iff_commute {α : Type u_3} {r : Relation α α} [inst : r.IsEquivalence] {s : Relation α α} [inst' : s.IsEquivalence] : (r.comp s).IsEquivalence ↔ r.comp s = s.comp r

@[reducible]

def Function.identified_under {α : Type u_3} {β : Type u_4} (f : α → β) : Relation α α

Equations

• Function.identified_under f a = (f a.fst = f a.snd)

@[simp]

theorem Function.mem_identified_under {α : Type u_3} {β : Type u_4} {f : α → β} {a a' : α} : (a, a') ∈ Function.identified_under f ↔ f a = f a'

instance Function.identified_under.isEquivalence {α : Type u_3} {β : Type u_4} {f : α → β} : (Function.identified_under f).IsEquivalence

Equations

• ⋯ = ⋯

@[simp]

theorem Quot.mk_eq_iff_rel {α : Type u_3} {r : Relation α α} [h : r.IsEquivalence] {a b : α} : Quot.mk (Function.curry r) a = Quot.mk (Function.curry r) b ↔ (a, b) ∈ r

@[simp]

theorem Quot.mk_surj {α : Type u_3} {r : Relation α α} : Function.Surjective (Quot.mk (Function.curry r))

@[simp]

theorem Relation.IsEquivalence.eq_identified_under {α : Type u_3} {r : Relation α α} [h : r.IsEquivalence] : Function.identified_under (Quot.mk (Function.curry r)) = r

def Relation.equiv_class {α : Type u_3} (r : Relation α α) (a : α) : Set α

Equations

• r.equiv_class a = {a' : α | (a, a') ∈ r ∧ (a', a) ∈ r}

@[simp]

theorem Relation.IsEquivalence.mem_equiv_class_iff {α : Type u_3} {r : Relation α α} [h : r.IsEquivalence] {a a' : α} : a ∈ r.equiv_class a' ↔ (a', a) ∈ r

@[simp]

theorem Relation.IsEquivalence.equiv_class_eq_iff {α : Type u_3} {r : Relation α α} {a a' : α} [h : r.IsEquivalence] : r.equiv_class a = r.equiv_class a' ↔ (a, a') ∈ r

@[simp]

theorem Relation.IsEquivalence.mem_equiv_class {α : Type u_3} {r : Relation α α} [h : r.IsEquivalence] {a : α} : a ∈ r.equiv_class a

theorem Relation.IsEquivalence.mem_equiv_class_swap {α : Type u_3} {r : Relation α α} [h : r.IsEquivalence] {a a' : α} : a ∈ r.equiv_class a' ↔ a' ∈ r.equiv_class a

def Relation.IsEquivalence.quot_equiv_class_bij {α : Type u_3} {r : Relation α α} [h : r.IsEquivalence] : Function.Bijection (Quot (Function.curry r)) ↥(r.equiv_class '' Set.univ)

Equations

• Relation.IsEquivalence.quot_equiv_class_bij = ⟨Quot.lift (Function.corestrict (fun (a : α) => r.equiv_class a) ⋯) ⋯, ⋯⟩

@[simp]

theorem Relation.equiv_class_diag {α : Type u_3} {a : α} : Relation.diag.equiv_class a = {a}

@[simp]

theorem Relation.equiv_class_univ {α : Type u_3} {a : α} : Relation.equiv_class Set.univ a = Set.univ

theorem Relation.quotient_preimage_isPartition {α : Type u_3} {r : Relation α α} : Set.IsPartition fun (x : Quot (Function.curry r)) => Quot.mk (Function.curry r) ⁻¹' {a : Quot (Function.curry r) | a = x}

theorem Set.IsPartition.in_same_equiv {α : Type u_3} {ι : Type u_5} {p : ι → Set α} (h : Set.IsPartition p) : Relation.IsEquivalence fun (x : α × α) => match x with | (x, y) => ∃ (i : ι), x ∈ p i ∧ y ∈ p i

def Relation.compatible {α : Type u_3} {β : Type u_4} {r : Relation α α} (p : α → β) : Prop

Equations

• Relation.compatible p = ∀ {x x' : α}, x ∈ r.equiv_class x' → p x = p x'

@[simp]

theorem Relation.diag_compatible {α : Type u_3} {β : Type u_4} {p : α → β} : Relation.compatible p

def Relation.compatible.lift {α : Type u_3} {β : Type u_4} {r : Relation α α} {p : α → β} [inst : r.IsEquivalence] (h : Relation.compatible p) : Quot (Function.curry r) → β

Equations

• h.lift = Quot.lift p ⋯

@[simp]

theorem Relation.compatible.lift_iff {α : Type u_3} {β : Type u_4} {r : Relation α α} {p : α → β} {a : α} [r.IsEquivalence] (h : Relation.compatible p) : h.lift (Quot.mk (Function.curry r) a) = p a

def Relation.saturated {α : Type u_3} {r : Relation α α} (x : Set α) : Prop

Equations

• Relation.saturated x = Relation.compatible fun (x_1 : α) => x_1 ∈ x

@[simp]

theorem Relation.IsEquivalence.saturated_iff {α : Type u_3} {r : Relation α α} [inst : r.IsEquivalence] {x : Set α} : Relation.saturated x ↔ ∀ (a : α), a ∈ x → r.equiv_class a ⊆ x

theorem Relation.IsEquivalence.saturated_iff_preimage_image_quotient {α : Type u_3} {r : Relation α α} [inst : r.IsEquivalence] {x : Set α} : Relation.saturated x ↔ x = Quot.mk (Function.curry r) ⁻¹' (Quot.mk (Function.curry r) '' x)

theorem Relation.saturated_iUnion {α : Type u_3} {r : Relation α α} {ι : Type u_5} {x : ι → Set α} (h : ∀ (i : ι), Relation.saturated (x i)) : Relation.saturated (⋃ i : ι, x i)

theorem Relation.saturated_iInter {α : Type u_3} {r : Relation α α} {ι : Type u_5} {x : ι → Set α} (h : ∀ (i : ι), Relation.saturated (x i)) : Relation.saturated (⋂ i : ι, x i)

theorem Relation.saturated.inter {α : Type u_3} {r : Relation α α} {x y : Set α} (h : Relation.saturated x) (h' : Relation.saturated y) : Relation.saturated (x ∩ y)

theorem Relation.saturated.union {α : Type u_3} {r : Relation α α} {x y : Set α} (h : Relation.saturated x) (h' : Relation.saturated y) : Relation.saturated (x ∪ y)

theorem Relation.saturated.compl {α : Type u_3} {r : Relation α α} {x : Set α} (h : Relation.saturated x) : Relation.saturated xᶜ

def Relation.saturation {α : Type u_3} {r : Relation α α} (x : Set α) : Set α

Equations

• Relation.saturation x = Quot.mk (Function.curry r) ⁻¹' (Quot.mk (Function.curry r) '' x)

@[simp]

theorem Relation.isEquivalence.saturation_saturated {α : Type u_3} {r : Relation α α} [inst : r.IsEquivalence] {x : Set α} : Relation.saturated (Relation.saturation x)

@[simp]

theorem Relation.subset_saturation {α : Type u_3} {r : Relation α α} {x : Set α} : x ⊆ Relation.saturation x

theorem Relation.IsEquivalence.saturation_smallest {α : Type u_3} {r : Relation α α} [inst : r.IsEquivalence] {x y : Set α} (h : Relation.saturated y) : x ⊆ y ↔ Relation.saturation x ⊆ y

theorem Relation.IsEquivalence.saturation_eq_equivalence_class_union {α : Type u_3} {r : Relation α α} [inst : r.IsEquivalence] {x : Set α} : Relation.saturation x = ⋃ i : ↥x, r.equiv_class i.val

theorem Relation.IsEquivalence.compatible_iff_factors {α : Type u_3} {β : Type u_4} {r : Relation α α} [inst : r.IsEquivalence] {f : α → β} : Relation.compatible f ↔ ∃ (g : Quot (Function.curry r) → β), f = g ∘ Quot.mk (Function.curry r)

@[simp]

theorem Function.identified_under_compatible {α : Type u_3} {β : Type u_4} (f : α → β) : Relation.compatible f

@[simp]

theorem Relation.identified_under_compatible_lift_inj {α : Type u_3} {β : Type u_4} {f : α → β} : Function.Injective (Relation.compatible.lift ⋯)

@[simp]

theorem Relation.identified_under_compatible_lift_image {α : Type u_3} {β : Type u_4} {f : α → β} : Relation.compatible.lift ⋯ '' Set.univ = f '' Set.univ

theorem Function.decompose_inj_bij_surj {α : Type u_3} {β : Type u_4} (f : α → β) : ∃ (k : Quot (Function.curry (Function.identified_under f)) → ↥(Relation.compatible.lift ⋯ '' Set.univ)), f = Subtype.val ∘ k ∘ Quot.mk (Function.curry (Function.identified_under f))

def Relation.compatible_lift2 {α : Type u_3} {β : Type u_4} {r : Relation α α} {f : α → β} {s : Relation β β} [inst1 : s.IsEquivalence] (h : ∀ (x x' : α), (x, x') ∈ r → (f x, f x') ∈ s) : Quot (Function.curry r) → Quot (Function.curry s)

Equations

• Relation.compatible_lift2 h = Quot.lift (Quot.mk (Function.curry s) ∘ f) ⋯

theorem Relation.compatible_lift2_commutes {α : Type u_3} {β : Type u_4} {r : Relation α α} {f : α → β} {s : Relation β β} [inst1 : s.IsEquivalence] (h : ∀ (x x' : α), (x, x') ∈ r → (f x, f x') ∈ s) : Relation.compatible_lift2 h ∘ Quot.mk (Function.curry r) = Quot.mk (Function.curry s) ∘ f

@[simp]

theorem Relation.compatible_lift2_apply {α : Type u_3} {β : Type u_4} {r : Relation α α} {a : α} {f : α → β} {s : Relation β β} [inst1 : s.IsEquivalence] (h : ∀ (x x' : α), (x, x') ∈ r → (f x, f x') ∈ s) : Relation.compatible_lift2 h (Quot.mk (Function.curry r) a) = Quot.mk (Function.curry s) (f a)

theorem Relation.IsEquivalence.inverse_image_eq_identified_under {γ : Type u_2} {α : Type u_3} {r : Relation α α} [inst : r.IsEquivalence] {f : γ → α} : r.inverse_image f = Function.identified_under (Quot.mk (Function.curry r) ∘ f)

@[simp]

theorem Relation.compatible_lift2_of_subtype_inj {α : Type u_3} {r : Relation α α} {x : Set α} [inst : r.IsEquivalence] : Function.Injective (Relation.compatible_lift2 ⋯)

@[simp]

theorem Relation.IsEquivalence.diag_subset {α : Type u_3} {r : Relation α α} [inst : r.IsEquivalence] : Relation.diag ⊆ r

def Relation.IsEquivalence.quotient_subset_map {α : Type u_3} {r : Relation α α} [r.IsEquivalence] {s : Relation α α} (h : r ⊆ s) : Quot (Function.curry r) → Quot (Function.curry s)

Equations

• Relation.IsEquivalence.quotient_subset_map h = Quot.lift (Quot.mk (Function.curry s)) ⋯

def Relation.IsEquivalence.quotient {α : Type u_3} {r : Relation α α} [r.IsEquivalence] {s : Relation α α} (h : r ⊆ s) : Relation (Quot (Function.curry r)) (Quot (Function.curry r))

Equations

• Relation.IsEquivalence.quotient h = Function.identified_under (Quot.lift (Quot.mk (Function.curry s)) ⋯)

theorem Relation.IsEquivalence.equiv_quotient_iff {α : Type u_3} {r : Relation α α} {a a' : α} [inst : r.IsEquivalence] {s : Relation α α} [inst' : s.IsEquivalence] (h : r ⊆ s) : (Quot.mk (Function.curry r) a, Quot.mk (Function.curry r) a') ∈ Relation.IsEquivalence.quotient h ↔ (a, a') ∈ s

def Relation.IsEquivalence.quotient_quotient {α : Type u_3} {r : Relation α α} [inst : r.IsEquivalence] {s : Relation α α} [inst' : s.IsEquivalence] (h : r ⊆ s) : Quot (Function.curry (Relation.IsEquivalence.quotient h)) → Quot (Function.curry s)

Equations

• Relation.IsEquivalence.quotient_quotient h = Quot.lift (Relation.IsEquivalence.quotient_subset_map h) ⋯

@[simp]

theorem Relation.IsEquivalence.quotient_quotient_bij {α : Type u_3} {r : Relation α α} [inst : r.IsEquivalence] {s : Relation α α} [inst' : s.IsEquivalence] (h : r ⊆ s) : Function.Bijective (Relation.IsEquivalence.quotient_quotient h)

theorem Relation.IsEquivalence.is_quotient_quotient {α : Type u_3} {r : Relation α α} [inst : r.IsEquivalence] {s : Relation (Quot (Function.curry r)) (Quot (Function.curry r))} [inst1 : s.IsEquivalence] : s = Relation.IsEquivalence.quotient ⋯

instance instIsEquivalenceProdProd_rel {α : Type u_3} {β : Type u_4} {r : Relation α α} {s : Relation β β} [inst : r.IsEquivalence] [inst' : s.IsEquivalence] : (r.prod_rel s).IsEquivalence

Equations

• ⋯ = ⋯

@[simp]

theorem Relation.IsEquivalence.prod_rel_equivalence_class {α : Type u_3} {β : Type u_4} {r : Relation α α} {s : Relation β β} [inst : r.IsEquivalence] [inst' : s.IsEquivalence] {a : α} {b : β} : (r.prod_rel s).equiv_class (a, b) = (r.equiv_class a).prod (s.equiv_class b)

theorem Relation.IsEquivalence.prod_rel_is_identified_under {α : Type u_3} {β : Type u_4} {r : Relation α α} {s : Relation β β} [inst : r.IsEquivalence] [inst' : s.IsEquivalence] : r.prod_rel s = Function.identified_under (Function.prod (Quot.mk (Function.curry r)) (Quot.mk (Function.curry s)))

def Relation.IsEquivalence.prod_quotient {α : Type u_3} {β : Type u_4} {r : Relation α α} {s : Relation β β} [inst : r.IsEquivalence] [inst' : s.IsEquivalence] : Quot (Function.curry (r.prod_rel s)) → Quot (Function.curry r) × Quot (Function.curry s)

Equations

• Relation.IsEquivalence.prod_quotient = Quot.lift (Function.prod (Quot.mk (Function.curry r)) (Quot.mk (Function.curry s))) ⋯

theorem Relation.IsEquivalence.prod_quotient_bij {α : Type u_3} {β : Type u_4} {r : Relation α α} {s : Relation β β} [inst : r.IsEquivalence] [inst' : s.IsEquivalence] : Function.Bijective Relation.IsEquivalence.prod_quotient

def Relation.IsEquivalence.powerset_quotient_subset_powerset {α : Type u_3} {x : Set α} : Function.Bijection (↥(𝒫 x)) (Quot (Function.curry (Function.identified_under fun (y : Set α) => x ∩ y)))

Equations

• One or more equations did not get rendered due to their size.

def Relation.IsEquivalence.quotient_image_bij_inverse_image {α : Type u_3} {β : Type u_4} {f : α → β} {r : Relation β β} [inst : r.IsEquivalence] : Function.Bijection (Quot (Function.curry (r.inverse_image f))) (Quot (Function.curry (r.restrict (f '' Set.univ))))

Equations

• Relation.IsEquivalence.quotient_image_bij_inverse_image = ⟨Relation.compatible_lift2 ⋯, ⋯⟩

def Quot.lift2_same {α : Type u_3} {β : Type u_4} (f : α → α → β) {r : α → α → Prop} [inst : Equivalence r] (h : ∀ (x x' y y' : α), r x x' → r y y' → f x y = f x' y') : Quot r → Quot r → β

Equations

• Quot.lift2_same f h = Quot.lift (fun (a : α) => Quot.lift (f a) ⋯) ⋯

@[simp]

theorem Quot.lift2_same_val {α : Type u_3} {β : Type u_4} {f : α → α → β} {r : α → α → Prop} [inst : Equivalence r] (h : ∀ (x x' y y' : α), r x x' → r y y' → f x y = f x' y') {a b : α} : Quot.lift2_same f h (Quot.mk r a) (Quot.mk r b) = f a b