ball_inter — Mathlib

English

In a uniform space, the ball around x with V ∩ W is exactly the intersection of the balls around x with V and with W.

Русский

В равномерном пространстве шар вокруг точки x с V ∩ W совпадает с пересечением шаров вокруг x с V и с W.

LaTeX

$$$\{ y \in \beta : (y, x) \in V \cap W \} = \{ y \in \beta : (y, x) \in V \} \cap \{ y \in \beta : (y, x) \in W \}$$$

Lean4

theorem ball_inter (x : β) (V W : Set (β × β)) : ball x (V ∩ W) = ball x V ∩ ball x W :=
  preimage_inter

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