mono_left

Mathlib.Topology.MetricSpace.MetricSeparated

URI: https://scilib.ai/kg/mathlib#Metric.AreSeparated.mono_left

English

If s' is separated from t and s ⊆ s', then s is separated from t.

Русский

Если S' отделено от T и S ⊆ S', тогда S отделено от T.

LaTeX

$$$ (s \subseteq s') \land \text{AreSeparated}(s',t) \Rightarrow \text{AreSeparated}(s,t) $$$

Lean4

theorem mono_left {s'} (h' : AreSeparated s' t) (hs : s ⊆ s') : AreSeparated s t :=
  h'.mono hs Subset.rfl

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

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

Разделы

Аффилиация

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