iInf_iUnion — Mathlib

English

Dual to iSup_iUnion: in a complete lattice, the infimum over a ∈ ⋃ i, s i of f a equals the infimum over i of the infimum over a ∈ s i of f a.

Русский

Кратно двойственно iSup_iUnion: двойная инфимум над a в ∪i si f(a) равна инфимууму по i от инфимума по a ∈ si f(a).

LaTeX

$$$\\bigwedge_{a \\in \\bigcup_i s_i} f(a) = \\bigwedge_i \\bigwedge_{a \\in s_i} f(a)$$$

Lean4

theorem iInf_iUnion (s : ι → Set α) (f : α → β) : ⨅ a ∈ ⋃ i, s i, f a = ⨅ (i) (a ∈ s i), f a :=
  iSup_iUnion (β := βᵒᵈ) s f

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