finite_isBounded_inter_isClosed — Mathlib

English

In a proper space α, if K is bounded and s is closed, and s has discrete topology, then K ∩ s is finite.

Русский

В правильном пространстве α, если K ограничено, s замкнуто и обладает дискретной топологией, то K∩s конечно.

LaTeX

$$$[ProperSpace\ α] \Rightarrow [DiscreteTopology\ s] \Rightarrow IsBounded(K) \Rightarrow IsClosed(s) \Rightarrow (K \cap s)\text{ finite}$$$

Lean4

theorem finite_isBounded_inter_isClosed [ProperSpace α] {K s : Set α} [DiscreteTopology s] (hK : IsBounded K)
    (hs : IsClosed s) : Set.Finite (K ∩ s) :=
  by
  refine Set.Finite.subset (IsCompact.finite ?_ ?_) (Set.inter_subset_inter_left s subset_closure)
  · exact hK.isCompact_closure.inter_right hs
  · exact DiscreteTopology.of_subset inferInstance Set.inter_subset_right

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