edistLtTopSetoid

Mathlib.Topology.EMetricSpace.Defs

URI: https://scilib.ai/kg/mathlib#EMetric.edistLtTopSetoid

Lean4

/-- Relation “two points are at a finite edistance” is an equivalence relation. -/
def edistLtTopSetoid : Setoid α where
  r x y := edist x y < ⊤
  iseqv :=
    ⟨fun x => by rw [edist_self]; exact ENNReal.coe_lt_top, fun h => by rwa [edist_comm], fun hxy hyz =>
      lt_of_le_of_lt (edist_triangle _ _ _) (ENNReal.add_lt_top.2 ⟨hxy, hyz⟩)⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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