English
For a ConditionallyCompleteLattice M and Nonempty ι, the support of the pointwise supremum of f(i) over i is contained in the union of supports of f(i): mulSupport (λ x. ⨆ i, f(i)(x)) ⊆ ⋃ i, mulSupport (f(i)).
Русский
Пусть M — условно совершенная решетка, ι не пусто. Опора функции x ↦ ⨆_i f(i)(x) лежит в объединении опор функций f(i).
LaTeX
$$$\\text{mulSupport}(\\lambda x. \\bigvee_{i} f(i)(x)) \\subseteq \\bigcup_{i} \\text{mulSupport}(f(i)).$$$
Lean4
@[to_additive]
theorem mulSupport_iSup [ConditionallyCompleteLattice M] [Nonempty ι] (f : ι → α → M) :
mulSupport (fun x ↦ ⨆ i, f i x) ⊆ ⋃ i, mulSupport (f i) :=
by
simp only [mulSupport_subset_iff', mem_iUnion, not_exists, notMem_mulSupport]
intro x hx
simp only [hx, ciSup_const]
