ite_eq_right_iff — Mathlib

English

Let α be a type, P a decidable proposition, and a,b ∈ α with a ≠ b. Then the right branch of the conditional expression equals b if and only if not P holds; i.e. ite P a b = b ⇔ ¬P, under a ≠ b.

Русский

Пусть α — множество, P — решаемое предложение, и a,b ∈ α с a ≠ b. Тогда правая ветвь условного выражения равна b тогда и только тогда, когда не выполняется P; т.е. ite P a b = b ⇔ ¬P при a ≠ b.

LaTeX

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

Lean4

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

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