ofIff — Mathlib

English

Equivalence between propositions is equivalent to logical equivalence: from P ↔ Q to P ≃ Q and back.

Русский

Эквивалентность между утверждениями равносильна логическому эквиваленту: из P ↔ Q в P ≃ Q и обратно.

LaTeX

$$$\\text{ofIff}: P \\iff Q \\longleftrightarrow P \\equiv Q$$$

Lean4

/-- equivalence of propositions is the same as iff -/
def ofIff {P Q : Prop} (h : P ↔ Q) : P ≃ Q :=
  ⟨h.mp, h.mpr, fun _ => rfl, fun _ => rfl⟩

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