support_sup — Mathlib

English

The supremum (coordinatewise) has support equal to the union of supports: (f ⊔ g).support = f.support ∪ g.support.

Русский

Наибольшая верхняя граница по координатам имеет опору, равную объединению опор: (f ⊔ g).support = f.support ∪ g.support.

LaTeX

$$$(f \vee g).\mathrm{support} = f.\mathrm{support} \cup g.\mathrm{support}$$$

Lean4

@[simp]
theorem support_sup : (f ⊔ g).support = f.support ∪ g.support :=
  by
  ext
  simp only [Finset.mem_union, mem_support_iff, sup_apply, Ne, ← nonpos_iff_eq_zero, sup_le_iff,
    Classical.not_and_iff_not_or_not]

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