support_inf_union_support_sup — Mathlib

English

Suppose ι is index set, α_i are lattices, and f,g are DFinsupp with decidable equality and decidable zero. Then the support of f ⊓ g united with the support of f ⊔ g equals the union of the supports of f and g.

Русский

Пусть ι — множество индексов, α_i — решетки, f,g — DFinsupp с разрешимым равенством и нулем. Тогда опора f ⊓ g объединенная с опорой f ⊔ g равна объединению опор f и g.

LaTeX

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

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]

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