dite_eq_left_iff — Mathlib

English

If for all h, a ≠ B h, then dite P (λ _ , a) B = a is equivalent to P.

Русский

Если для всех h выполняется a ≠ B h, то dite P (λ _ , a) B = a эквивалентно P.

LaTeX

$$$(\mathrm{dite}\, P\,(\lambda\_\to a)\, B)=a \iff P,$ при условии $\forall h, a \neq B(h)$.$$

Lean4

protected theorem dite_eq_left_iff (h : ∀ h, a ≠ B h) : dite P (fun _ ↦ a) B = a ↔ P :=
  dite_eq_left_iff.trans ⟨fun H ↦ of_not_not fun h' ↦ h h' (H h').symm, fun h H ↦ (H h).elim⟩

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