imp_iff_right_iff

Mathlib.Logic.Basic

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

English

For propositions a,b, the statement (a → b) ↔ b is logically equivalent to a ∨ b.

Русский

Для утверждений a,b логически эквивалентно (a → b) ↔ b эквивалентно a ∨ b.

LaTeX

$$$ (a \\rightarrow b \\leftrightarrow b) \\;\\iff\\; a \\lor b. $$$

Lean4

theorem imp_iff_right_iff {a b : Prop} : (a → b ↔ b) ↔ a ∨ b :=
  open scoped Classical in Decidable.imp_iff_right_iff

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

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

Разделы

Аффилиация

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