supported_union — Mathlib

English

The supported submodule on a union equals the join of the two supports.

Русский

Подмодуль на объединении равен объединению двух опор.

LaTeX

$$$\mathrm{supported}(M,R,(s \cup t)) = \mathrm{supported}(M,R,s) \;\sqcup\; \mathrm{supported}(M,R,t)$$$

Lean4

theorem supported_union (s t : Set α) : supported M R (s ∪ t) = supported M R s ⊔ supported M R t := by
  rw [Set.union_eq_iUnion, supported_iUnion, iSup_bool_eq, cond_true, cond_false]

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