rel_iff_exists_classes — Mathlib

English

For a setoid r on α, two elements x,y are related iff there exists a class c in r.classes containing both x and y.

Русский

Для заданного множества эквивалентности r на α элементы x и y связаны, если существует класс c из r.classes, который содержит и x, и y.

LaTeX

$$$r(x,y) \\iff \\exists c \\in r.classes, x \\in c \\wedge y \\in c.$$$

Lean4

theorem rel_iff_exists_classes (r : Setoid α) {x y} : r x y ↔ ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c :=
  ⟨fun h => ⟨_, r.mem_classes y, h, r.refl' y⟩, fun ⟨c, ⟨z, hz⟩, hx, hy⟩ =>
    by
    subst c
    exact r.trans' hx (r.symm' hy)⟩

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