dite_prop_iff_or — Mathlib

English

The dite P Q R is equivalent to either ∃h, Q h or ∃h, R h, i.e., dite P Q R ↔ (∃ h, Q h) ∨ (∃ h, R h).

Русский

Dite P Q R эквивалентен либо существованию h с Q h, либо существованию h с R h.

LaTeX

$$$\dite P Q R \iff \big(\exists h, Q h\big) \lor \big(\exists h, R h\big)$$$

Lean4

theorem dite_prop_iff_or {Q : P → Prop} {R : ¬P → Prop} : dite P Q R ↔ (∃ p, Q p) ∨ (∃ p, R p) := by
  by_cases h : P <;>
    simp [h, exists_prop_of_false, exists_prop_of_true]
      -- TODO make this a simp lemma in a future PR

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