dite_eq_right_iff — Mathlib

English

If for all h, A h ≠ b, then (dite P A (λ _ , b)) = b is equivalent to ¬P.

Русский

Если для всех h, A(h) ≠ b, тогда (dite P A (λ _ , b)) = b эквивалентно ¬P.

LaTeX

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

Lean4

protected theorem dite_eq_right_iff (h : ∀ h, A h ≠ b) : (dite P A fun _ ↦ b) = b ↔ ¬P :=
  dite_eq_right_iff.trans ⟨fun H h' ↦ h h' (H h'), fun h' H ↦ (h' H).elim⟩

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