mem_dite_univ_left — Mathlib

English

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

Русский

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

LaTeX

$$$ x \\in \\mathrm{if}\\ h : p \\mathrm{ then } \\mathrm{univ} \\mathrm{ else } t h \\iff \\forall h : \\neg p, x \\in t h $$$

Lean4

theorem mem_dite_univ_left (p : Prop) [Decidable p] (t : ¬p → Set α) (x : α) :
    (x ∈ if h : p then univ else t h) ↔ ∀ h : ¬p, x ∈ t h := by split_ifs <;> simp_all

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