instMaxOfAddLeftMonoOfAddRightMono

English

The pointwise maximum of two pseudo metrics d and d' defines a pseudo metric: (d ∨ d')(x,y) = max{d(x,y), d'(x,y)}.

Русский

Пусть d и d' — два псевдометра; их точечное максимальное объединение (d ∨ d')(x,y)=max{d(x,y), d'(x,y)} образует псевдометрику.

LaTeX

$$$(d \vee d')(x,y) = \max\{d(x,y), d'(x,y)\}$ defines a pseudo metric on X.$$

Lean4

instance [AddZeroClass R] [SemilatticeSup R] [AddLeftMono R] [AddRightMono R] : Max (PseudoMetric X R) where
  max d
    d' :=
    { toFun := fun x y ↦ (d x y) ⊔ (d' x y)
      refl' _ := by simp
      symm' x y := by simp [d.symm, d'.symm]
      triangle' := by
        intro x y z
        simp only [sup_le_iff]
        refine ⟨(d.triangle x y z).trans ?_, (d'.triangle x y z).trans ?_⟩ <;> apply add_le_add <;> simp }

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