eq_top_iff — Mathlib

English

Let s be an equivalence relation on α. Then s equals the universal relation iff for all x,y in α, x and y are related by s.

Русский

Пусть s — отношение эквивалентности на α. Тогда s = ⊤ тогда и только тогда, когда для всех x,y ∈ α выполняется x ∼_s y.

LaTeX

$$$$ s = \\top \\iff \\forall x,y:\\alpha,\\ s\\,x\,y. $$$$

Lean4

theorem eq_top_iff {s : Setoid α} : s = (⊤ : Setoid α) ↔ ∀ x y : α, s x y :=
  by
  rw [_root_.eq_top_iff, Setoid.le_def, Setoid.top_def]
  simp only [Pi.top_apply, «Prop».top_eq_true, forall_true_left]

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