flip_eq — Mathlib

English

Let r be a symmetric relation on a type α. Then flip r equals r.

Русский

Пусть r — симметричное отношение на множество α. Тогда перевернутое отношение flip r равно r.

LaTeX

$$$\forall \alpha\,\forall r:\alpha\to\alpha\to \mathrm{Prop},\; \mathrm{Symmetric}(r) \Rightarrow \mathrm{flip}(r) = r$$$

Lean4

theorem flip_eq (h : Symmetric r) : flip r = r :=
  funext₂ fun _ _ ↦ propext <| h.iff _ _

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