dite_eq_iff' — Mathlib

English

The equality (dite P A B) = c holds iff for all h, A h = c and for all h, B h = c.

Русский

Равенство (dite P A B) = c верно тогда, когда для всех h выполняется A h = c и для всех h выполняется B h = c.

LaTeX

$$$(\mathrm{dite}\, P\, A\, B)=c \iff (\forall h\, A(h)=c) \land (\forall h\, B(h)=c).$$$

Lean4

theorem dite_eq_iff' : dite P A B = c ↔ (∀ h, A h = c) ∧ ∀ h, B h = c :=
  ⟨fun he ↦ ⟨fun h ↦ (dif_pos h).symm.trans he, fun h ↦ (dif_neg h).symm.trans he⟩, fun he ↦
    (em P).elim (fun h ↦ (dif_pos h).trans <| he.1 h) fun h ↦ (dif_neg h).trans <| he.2 h⟩

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