closure_mono — Mathlib

English

Let L be a language and M a structure. If s ⊆ t are subsets of M, then the closure of s is contained in the closure of t. In other words, the closure operator is monotone with respect to inclusion.

Русский

Пусть L — язык, M — структура. Если s ⊆ t — подмножества M, то замыкание s содержится в замыкании t; замыкание по отношению к включению монотонно.

LaTeX

$$$$ s \subseteq t \Rightarrow \operatorname{closure}_L(s) \le \operatorname{closure}_L(t) $$$$

Lean4

/-- Substructure closure of a set is monotone in its argument: if `s ⊆ t`,
then `closure L s ≤ closure L t`. -/
@[gcongr]
theorem closure_mono ⦃s t : Set M⦄ (h : s ⊆ t) : closure L s ≤ closure L t :=
  (closure L).monotone h

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