mem_dite_univ_right — Mathlib

English

For any p and any family t : p → Set α, the membership x ∈ if h : p then t h else univ is equivalent to ∀ h : p, x ∈ t h.

Русский

Для любого p и семейства t : p → Set α членство x ∈ if h : p then t h else univ эквивалентно ∀ h : p, x ∈ t h.

LaTeX

$$$ (x \\in \\mathrm{if}\ h : p \\mathrm{ then } t h \\mathrm{ else } \\mathrm{univ}) \\ \\Leftrightarrow \\ \\forall h : p, x \\in t h $$$

Lean4

theorem mem_dite_univ_right (p : Prop) [Decidable p] (t : p → Set α) (x : α) :
    (x ∈ if h : p then t h else univ) ↔ ∀ h : p, x ∈ t h := by simp [mem_dite]

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