ite_eq_or_eq — Mathlib

English

For any Prop P, Q and α, the equation ite P a b = a ∨ ite P a b = b holds; i.e., the result is either a or b depending on the truth value of P.

Русский

Для любых propositions P, Q и множества α утверждается: ite P a b равно либо a, либо b; тождество говорит, что результат равен одной из ветвей в зависимости от истинности P.

LaTeX

$$ite P a b = a \vee ite P a b = b$$

Lean4

theorem ite_eq_or_eq : ite P a b = a ∨ ite P a b = b :=
  if h : _ then .inl (if_pos h) else .inr (if_neg h)

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