exists_of_mem_partition — Mathlib

English

Every element of α lying in the partition c belongs to the equivalence class of some y: there exists y with s = {x | x ∼ y}.

Русский

Каждый элемент α, принадлежащий разбиению c, лежит в классе эквивалентности некоторого элемента y: существует y такой, что s = {x | x ∼ y}.

LaTeX

$$$\\exists y\\, s = \\{x \\mid r(x,y)\\}$ where r is the equivalence relation induced by c$$

Lean4

/-- All elements of a partition of α are the equivalence class of some y ∈ α. -/
theorem exists_of_mem_partition {c : Set (Set α)} (hc : IsPartition c) {s} (hs : s ∈ c) :
    ∃ y, s = {x | mkClasses c hc.2 x y} :=
  let ⟨y, hy⟩ := nonempty_of_mem_partition hc hs
  ⟨y, eq_eqv_class_of_mem hc.2 hs hy⟩

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