mem_dite_empty_right — Mathlib

English

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

Русский

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

LaTeX

$$$ x \\in \\mathrm{if}\\ h : p \\mathrm{ then } t h \\mathrm{ else } \\emptyset \\iff \\exists h : p, x \\in t h $$$

Lean4

theorem mem_dite_empty_right (p : Prop) [Decidable p] (t : p → Set α) (x : α) :
    (x ∈ if h : p then t h else ∅) ↔ ∃ h : p, x ∈ t h :=
  by
  simp only [mem_dite, mem_empty_iff_false, imp_false, not_not]
  exact ⟨fun h => ⟨h.2, h.1 h.2⟩, fun ⟨h₁, h₂⟩ => ⟨fun _ => h₂, h₁⟩⟩

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