fromRel_top — Mathlib

English

If the relation is always true, fromRel is universal (the entire set of unordered pairs).

Русский

Если отношение тождественно истинно, fromRel охватывает все неупорядоченные пары.

LaTeX

$$$$ \mathrm{fromRel}(\mathrm{\top}) = \mathrm{Set.univ}. $$$$

Lean4

theorem fromRel_top : fromRel (fun (_ _ : α) z => z : Symmetric ⊤) = Set.univ :=
  by
  apply Set.eq_univ_of_forall fun e => _
  apply Sym2.ind
  simp [-Set.top_eq_univ, «Prop».top_eq_true]

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