limsup_sdiff — Mathlib

English

In a Boolean algebra, removing a fixed element a from limsup can be computed as limsup of the pointwise differences: limsup u f \\ a = limsup (λ b. u b \\ a) f.

Русский

В булевой алгебре разность лимсупа с фиксированным элементом a равна лимсупу от точечных разностей: limsup u f \\ a = limsup (λ b. u b \\ a) f.

LaTeX

$$$\\limsup u f \\setminus a = \\limsup (\\lambda b. (u b) \\setminus a) f$$$

Lean4

theorem limsup_sdiff (a : α) : limsup u f \ a = limsup (fun b => u b \ a) f :=
  by
  simp only [limsup_eq_iInf_iSup, sdiff_eq]
  rw [biInf_inf (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]
  simp_rw [inf_comm, inf_iSup₂_eq, inf_comm]

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