instTotallySeparatedSpaceOfIsUltrametricDist

English

A space with an ultrametric is totally separated: for any distinct x,y there exists a clopen ball B(x,r) with y ∉ B(x,r).

Русский

Пространство с ультраметрическим расстоянием полностью разобщено: для любых различных x,y существует клипошар B(x,r) с тем, что y не принадлежит B(x,r).

LaTeX

$$∀ x ≠ y, ∃ r > 0, IsClopen(\mathrm{ball}(x,r)) ∧ y ∉ \mathrm{ball}(x,r)$$

Lean4

instance {X : Type*} [MetricSpace X] [IsUltrametricDist X] : TotallySeparatedSpace X :=
  totallySeparatedSpace_iff_exists_isClopen.mpr fun x y h ↦
    by
    obtain ⟨r, hr, hr'⟩ := exists_between (dist_pos.mpr h)
    refine ⟨_, IsUltrametricDist.isClopen_ball x r, ?_, ?_⟩
    · simp only [mem_ball, dist_self, hr]
    · simp only [Set.mem_compl, mem_ball, dist_comm, not_lt, hr'.le]

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