ball_iInter — Mathlib

English

For any family V_i of relations, the ball around x with the intersection over i of V_i equals the intersection over i of the balls around x with V_i.

Русский

Для семейства отношений V_i шар вокруг x по пересечению по i равен пересечению шаров вокруг x по V_i.

LaTeX

$$$\operatorname{ball}(x, \bigcap_i V_i) = \bigcap_i \operatorname{ball}(x, V_i)$$$

Lean4

theorem ball_iInter {x : β} {V : ι → Set (β × β)} : ball x (⋂ i, V i) = ⋂ i, ball x (V i) :=
  preimage_iInter

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