ite_ne_left_iff

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#Ne.ite_ne_left_iff

English

Let α be a type, P a decidable proposition, and a,b ∈ α with a ≠ b. Then ite P a b ≠ a iff not P.

Русский

Пусть α — множество, P — решаемое, a ≠ b. Тогда ite P a b ≠ a эквивалентно ¬P.

LaTeX

$$(a \neq b) \rightarrow (\operatorname{ite} P a b \neq a \iff \lnot P)$$

Lean4

protected theorem ite_ne_left_iff (h : a ≠ b) : ite P a b ≠ a ↔ ¬P :=
  Ne.dite_ne_left_iff fun _ ↦ h

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

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

Разделы

Аффилиация

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