mem_dite — Mathlib

English

For membership in a dite, (a ∈ if h : p then s h else t h) holds exactly when a belongs to s h for all h and to t h for all h.

Русский

Для принадлежности в dite выполняется: a принадлежит s h для всех h при истинности p и a принадлежит t h для всех h при ложности p.

LaTeX

$$$(a \in \text{if } h : p \text{ then } s h \text{ else } t h) \iff (\forall h, a \in s h) \land (\forall h, a \in t h)$$$

Lean4

theorem mem_dite {a : α} {s : p → β} {t : ¬p → β} :
    (a ∈ if h : p then s h else t h) ↔ (∀ h, a ∈ s h) ∧ (∀ h, a ∈ t h) := by by_cases h : p <;> simp [h]

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