ball_zero_eq — Mathlib

English

The closedBall of the supremum p ⊔ q equals the intersection of the closedBalls: closedBall(p ⊔ q) e r = closedBall(p) e r ∩ closedBall(q) e r.

Русский

Замкнутый шар над максимальным шаром равен пересечению замкнутых шаров: closedBall(p ⊔ q) e r = closedBall(p) e r ∩ closedBall(q) e r.

LaTeX

$$$\\mathrm{closedBall}_{p \\sqcup q}(e,r) = \\mathrm{closedBall}_p(e,r) \\cap \\mathrm{closedBall}_q(e,r)$$$

Lean4

theorem ball_zero_eq : ball p 0 r = {y : E | p y < r} :=
  Set.ext fun _ => p.mem_ball_zero

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