mono_right

Mathlib.Topology.MetricSpace.MetricSeparated

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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