mulSupport_iInf — Mathlib

English

For a ConditionallyCompleteLattice M and Nonempty ι, the support of the pointwise infimum of f(i) over i is contained in the union of supports of f(i): mulSupport (λ x. iInf i, f(i)(x)) ⊆ ⋃ i, mulSupport (f i).

Русский

Пусть M — условно совершенная решетка, ι непусто. Опора x ↦ ⨅_i f(i)(x) лежит в объединении опор функций f(i).

LaTeX

$$$\\text{mulSupport}(\\lambda x. \\bigwedge_{i} f(i)(x)) \\subseteq \\bigcup_{i} \\text{mulSupport}(f(i)).$$$

Lean4

@[to_additive]
theorem mulSupport_iInf [ConditionallyCompleteLattice M] [Nonempty ι] (f : ι → α → M) :
    mulSupport (fun x ↦ ⨅ i, f i x) ⊆ ⋃ i, mulSupport (f i) :=
  mulSupport_iSup (M := Mᵒᵈ) f

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