einfsep_anti — Mathlib

English

Let s and t be subsets with s ⊆ t in a metric-like space. Then the distance separation of t is no larger than that of s; i.e. enfsep is monotone nonincreasing with respect to set inclusion.

Русский

Пусть s и t — подмножества, причём s ⊆ t. Тогда einfsep(t) не больше einfsep(s); то есть функция einfsep инерционна по включениям.

LaTeX

$$$ (s \subseteq t) \Rightarrow t.einfsep \le s.einfsep $$$

Lean4

theorem einfsep_anti (hst : s ⊆ t) : t.einfsep ≤ s.einfsep :=
  le_einfsep fun _x hx _y hy => einfsep_le_edist_of_mem (hst hx) (hst hy)

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