sInf_sUnion — Mathlib

English

Dual of sSup_sUnion: the infimum of the union of a collection of sets equals the infimum over the collection of infima.

Русский

Двойственно sSup_sUnion: инфиминум объединения множества равен инфиминуму над всей коллекцией.

LaTeX

$$$sInf(\\bigcup s) = \\bigwedge_{t \\in s} sInf(t)$$$

Lean4

theorem sInf_sUnion (s : Set (Set β)) : sInf (⋃₀ s) = ⨅ t ∈ s, sInf t :=
  sSup_sUnion (β := βᵒᵈ) s

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