class_of — Mathlib

English

For any x ∈ α, the equivalence class of x under hs.setoid coincides with s(hs.index x); i.e., setOf (hs.setoid x) = s (hs.index x).

Русский

Для любого x ∈ α класс эквивалентности x по hs.setoid совпадает с s(hs.index x); то есть setOf(hs.setoid x) = s(hs.index x).

LaTeX

$$$ \operatorname{setOf}(hs.setoid\; x) = s(hs.index\; x) $$$

Lean4

theorem class_of {x : α} : setOf (hs.setoid x) = s (hs.index x) :=
  Set.ext fun _y => eq_comm.trans hs.mem_iff_index_eq.symm

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