support_sup_union_support_inf — Mathlib

English

Similarly, the union of the supports of f ⊔ g and f ⊓ g equals the union of supports of f and g: (f ⊔ g).support ∪ (f ⊓ g).support = f.support ∪ g.support.

Русский

Аналогично: опора (f ⊔ g) ∪ опора (f ⊓ g) равна опоре f ∪ опоре g.

LaTeX

$$$ (f \\vee g).support \\cup (f \\wedge g).support = f.support \\cup g.support $$$

Lean4

theorem support_sup_union_support_inf : (f ⊔ g).support ∪ (f ⊓ g).support = f.support ∪ g.support :=
  (union_comm _ _).trans <| support_inf_union_support_sup _ _

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