Description: The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | remet.1 | ⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) | |
Assertion | rexmet | ⊢ 𝐷 ∈ ( ∞Met ‘ ℝ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | remet.1 | ⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) | |
2 | 1 | remet | ⊢ 𝐷 ∈ ( Met ‘ ℝ ) |
3 | metxmet | ⊢ ( 𝐷 ∈ ( Met ‘ ℝ ) → 𝐷 ∈ ( ∞Met ‘ ℝ ) ) | |
4 | 2 3 | ax-mp | ⊢ 𝐷 ∈ ( ∞Met ‘ ℝ ) |