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]