support_sup_union_support_inf — Mathlib

English

The supports satisfy symmetrically: the union of the supports of f ⊔ g and f ⊓ g equals the union of supports of f and g.

Русский

Опоры удовлетворяют симметрично: объединение опор f ⊔ g и f ⊓ g равно объединению опор f и g.

LaTeX

$$$$ \operatorname{supp}(f \sup g) \cup \operatorname{supp}(f \inf g) = \operatorname{supp}(f) \cup \operatorname{supp}(g). $$$$

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 _ _

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