mem_ball_comp — Mathlib

English

If y ∈ ball x V and z ∈ ball y W, then z ∈ ball x (V ○ W).

Русский

Если y ∈ ball x V и z ∈ ball y W, то z ∈ ball x (V ○ W).

LaTeX

$$$$\\text{If } y ∈ ball\, x\, V\\text{ and } z ∈ ball\, y\, W\\text{ then } z ∈ ball\, x\, (V ○ W).$$$$

Lean4

/-- The triangle inequality for `UniformSpace.ball` -/
theorem mem_ball_comp {V W : Set (β × β)} {x y z} (h : y ∈ ball x V) (h' : z ∈ ball y W) : z ∈ ball x (V ○ W) :=
  prodMk_mem_compRel h h'

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