prod_sup_edist_ne_top_aux — Mathlib

English

For f, g ∈ WithLp ∞ (α × β) with pseudo-metric spaces on α, β, the supremum of the coordinate distances is strictly less than ∞.

Русский

Для f, g ∈ WithLp ∞ (α × β) с псевдометрическими пространствами на α, β супremum расстояний по координатам конечно меньше бесконечности.

LaTeX

$$$$\operatorname{edist} f.fst g.fst \sqcup \operatorname{edist} f.snd g.snd \neq \top$$$$

Lean4

/-- An auxiliary lemma used twice in the proof of `WithLp.prodPseudoMetricAux` below. Not intended
for use outside this file. -/
theorem prod_sup_edist_ne_top_aux [PseudoMetricSpace α] [PseudoMetricSpace β] (f g : WithLp ∞ (α × β)) :
    edist f.fst g.fst ⊔ edist f.snd g.snd ≠ ⊤ :=
  ne_of_lt <| by simp [edist, PseudoMetricSpace.edist_dist]

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