closure_mono

Mathlib.Topology.Closure

URI: https://scilib.ai/kg/mathlib#closure_mono

English

If s ⊆ t then closure s ⊆ closure t.

Русский

Если s ⊆ t, то closure s ⊆ closure t.

LaTeX

$$s \subseteq t \Rightarrow \overline{s} \subseteq \overline{t}$$

Lean4

@[mono, gcongr]
theorem closure_mono (h : s ⊆ t) : closure s ⊆ closure t :=
  closure_minimal (Subset.trans h subset_closure) isClosed_closure

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru