iff_isEquiv

Mathlib.Order.Defs.Unbundled

URI: https://scilib.ai/kg/mathlib#iff_isEquiv

English

Iff is an equivalence relation on propositions.

Русский

Iff является эквивалентностью на множествах высказываний.

LaTeX

$$IsEquiv Prop Iff$$

Lean4

/-- `Iff` is an equivalence relation. -/
instance iff_isEquiv : IsEquiv Prop Iff where
  symm := @Iff.symm
  trans := @Iff.trans
  refl := @Iff.refl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru