true_equivalence — Mathlib

English

There exists a trivial equivalence relation on any type α, namely the relation that holds for all pairs, and this relation is an equivalence relation.

Русский

Существует тривиальная эквивалентность на любом типе α, равная отношению истинности для любых пар, и она является эквивалентностью.

LaTeX

$$$\\text{Equivalence}(\\lambda x,y.\\ True)$$$

Lean4

theorem true_equivalence : @Equivalence α fun _ _ ↦ True :=
  ⟨fun _ ↦ trivial, fun _ ↦ trivial, fun _ _ ↦ trivial⟩

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