support_inf_union_support_sup — Mathlib

English

For finitely supported M-valued functions f and g, the support of their infimum and supremum satisfies the relation (f ⊓ g).support ∪ (f ⊔ g).support = f.support ∪ g.support.

Русский

Для функций с конечной опорой из ι в M выполняется: опора (f ⊓ g) ∪ опора (f ⊔ g) равна опоре f ∪ опоре g.

LaTeX

$$$ (f \\inf g).support \\cup (f \\sup g).support = f.support \\cup g.support $$$

Lean4

theorem support_inf_union_support_sup : (f ⊓ g).support ∪ (f ⊔ g).support = f.support ∪ g.support :=
  coe_injective <| compl_injective <| by ext; simp [inf_eq_and_sup_eq_iff]

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