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)