eq_eqv_class_of_mem — Mathlib

English

The equivalence class { x | mkClasses c H x y } is an element of the partition c.

Русский

Эквивалентный класс { x : α | mkClasses c H x y } принадлежит разбиению c.

LaTeX

$$$\\{ x \\mid \\mathrm{mkClasses}(c,H)(x,y) \\} \\in c$$$

Lean4

/-- The elements of a set of sets partitioning α are the equivalence classes of the
equivalence relation defined by the set of sets. -/
theorem eq_eqv_class_of_mem {c : Set (Set α)} (H : ∀ a, ∃! b ∈ c, a ∈ b) {s y} (hs : s ∈ c) (hy : y ∈ s) :
    s = {x | mkClasses c H x y} := by
  ext x
  constructor
  · intro hx _s' hs' hx'
    rwa [eq_of_mem_eqv_class H hs' hx' hs hx]
  · intro hx
    obtain ⟨b', ⟨hc, hb'⟩, _⟩ := H x
    rwa [eq_of_mem_eqv_class H hs hy hc (hx b' hc hb')]

Похожие утверждения