point_finite — Mathlib

English

Let f be a locally finite family of subsets of X. Then for every x in X, the set of indices b with x in f(b) is finite.

Русский

Пусть {f_i} — локально конечная семейство подмножеств X. Тогда для каждой точки x ∈ X множество индексов i таких, что x ∈ f_i, является конечным.

LaTeX

$$$\{b \in \iota \mid x \in f(b)\}. \text{Finite}$$$

Lean4

theorem point_finite (hf : LocallyFinite f) (x : X) : {b | x ∈ f b}.Finite :=
  let ⟨_t, hxt, ht⟩ := hf x
  ht.subset fun _b hb => ⟨x, hb, mem_of_mem_nhds hxt⟩

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