infsep_anti

Mathlib.Topology.MetricSpace.Infsep

URI: https://scilib.ai/kg/mathlib#Set.Nontrivial.infsep_anti

English

If s is nontrivial and s ⊆ t, then t.infsep ≤ s.infsep.

Русский

Если s не тривиально и s ⊆ t, то t.infsep ≤ s.infsep.

LaTeX

$$$ \text{hs} : s.Nontrivial \rightarrow (s \subseteq t) \rightarrow t.infsep \le s.infsep $$$

Lean4

theorem infsep_anti (hs : s.Nontrivial) (hst : s ⊆ t) : t.infsep ≤ s.infsep :=
  ENNReal.toReal_mono hs.einfsep_ne_top (einfsep_anti hst)

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

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

Разделы

Аффилиация

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