or_congr_right'

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#or_congr_right'

English

For any a,b,c: if ¬a → (b ↔ c), then a ∨ b ↔ a ∨ c.

Русский

Для любых a,b,c: если ¬a → (b ⇔ c), то a ∨ b ⇔ a ∨ c.

LaTeX

$$$ (\\neg a \\to (b \\leftrightarrow c)) \\rightarrow (a \\lor b) \\leftrightarrow (a \\lor c) $$$

Lean4

theorem or_congr_right' {c : Prop} (h : ¬a → (b ↔ c)) : a ∨ b ↔ a ∨ c :=
  open scoped Classical in Decidable.or_congr_right' h

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

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

Разделы

Аффилиация

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