sup_liminf — Mathlib

English

For NeBot f and a ∈ α, a ⊔ liminf u f = liminf (λ x. a ⊔ u x) f.

Русский

Для NeBot f и a ∈ α: a ⊔ liminf u f = liminf (λ x. a ⊔ u x) f.

LaTeX

$$$\\operatorname{sup}(a, \\operatorname{liminf} u f) = \\operatorname{liminf}(\\lambda x. a \\sqcup u x) f$$$

Lean4

theorem sup_liminf (a : α) : a ⊔ liminf u f = liminf (fun x => a ⊔ u x) f :=
  by
  simp only [liminf_eq_iSup_iInf]
  rw [sup_comm, biSup_sup (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]
  simp_rw [iInf₂_sup_eq, sup_comm (a := a)]

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