English
An outer measure constructed via mkMetric' is a metric outer measure.
Русский
Внешняя мера, построенная через mkMetric', является метрической внешней мерой.
LaTeX
$$$(\\mathrm{mkMetric'}(m)).\\mathrm{IsMetric}$$$
Lean4
/-- An outer measure constructed using `OuterMeasure.mkMetric'` is a metric outer measure. -/
theorem mkMetric'_isMetric (m : Set X → ℝ≥0∞) : (mkMetric' m).IsMetric :=
by
rintro s t ⟨r, r0, hr⟩
refine
tendsto_nhds_unique_of_eventuallyEq (mkMetric'.tendsto_pre _ _)
((mkMetric'.tendsto_pre _ _).add (mkMetric'.tendsto_pre _ _)) ?_
rw [← pos_iff_ne_zero] at r0
filter_upwards [Ioo_mem_nhdsGT r0]
rintro ε ⟨_, εr⟩
refine boundedBy_union_of_top_of_nonempty_inter ?_
rintro u ⟨x, hxs, hxu⟩ ⟨y, hyt, hyu⟩
have : ε < diam u := εr.trans_le ((hr x hxs y hyt).trans <| edist_le_diam_of_mem hxu hyu)
exact iInf_eq_top.2 fun h => (this.not_ge h).elim
