iUnion_inter_closedBall_nat

Mathlib.Topology.MetricSpace.Pseudo.Defs

URI: https://scilib.ai/kg/mathlib#Metric.iUnion_inter_closedBall_nat

← MathLib Explorer

English

For any subset s and any x, the union over n of s ∩ closedBall(x, n) equals s.

Русский

Для любого множества s и точки x ∈ α, объединение по n⋯ s ∩ B̄(x, n) даёт s.

LaTeX

$$$ \bigcup_{n \in \mathbb{N}} (s \cap \overline{B}(x, n)) = s $$$

Lean4

theorem iUnion_inter_closedBall_nat (s : Set α) (x : α) : ⋃ n : ℕ, s ∩ closedBall x n = s := by
  rw [← inter_iUnion, iUnion_closedBall_nat, inter_univ]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru