le_einfsep

Mathlib.Topology.MetricSpace.Infsep

URI: https://scilib.ai/kg/mathlib#Set.le_einfsep

English

If for all x ∈ s and y ∈ s with x ≠ y we have d ≤ edist x y, then d ≤ s.einfsep.

Русский

Если для всех x,y ∈ s с x ≠ y выполняется d ≤ edist x y, то d ≤ s.einfsep.

LaTeX

$$$\forall x \in s, \forall y \in s, x \neq y \Rightarrow d \le edist x y \implies d \le s.einfsep$$$

Lean4

theorem le_einfsep {d} (h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y) : d ≤ s.einfsep :=
  le_einfsep_iff.2 h

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

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

Разделы

Аффилиация

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