supported_mono — Mathlib

English

If s ⊆ t, then the corresponding supported subalgebras satisfy a inclusion: supported(R,s) ≤ supported(R,t).

Русский

Если s ⊆ t, то соответствующие поддерживаемые подалгебры удовлетворяют включению: supported(R,s) ≤ supported(R,t).

LaTeX

$$$$ \text{If } s \subseteq t, \quad \mathrm{supported}(R,s) \le \mathrm{supported}(R,t). $$$$

Lean4

theorem supported_mono (st : s ⊆ t) : supported R s ≤ supported R t :=
  Algebra.adjoin_mono (Set.image_mono st)

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