ite_eq_left_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

protected theorem ite_eq_left_iff (h : a ≠ b) : ite P a b = a ↔ P :=
  Ne.dite_eq_left_iff fun _ ↦ h

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