mem_dite_empty_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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