compl_mem_sets_of_nhdsWithin — Mathlib

English

The complement of a compact set belongs to a filter f if for each x ∈ s, sᶜ ∈ 𝓝 x ⊓ f.

Русский

Дополнение компактного множества принадлежит фильтру f, если для каждого x ∈ s окружение nt x ∩ f содержит sᶜ.

LaTeX

$$$ IsCompact s \to (\forall x \in s, s^c \in 𝓝 x \cap f) \to s^c \in f $$$

Lean4

/-- The complement to a compact set belongs to a filter `f` if each `x ∈ s` has a neighborhood `t`
within `s` such that `tᶜ` belongs to `f`. -/
theorem compl_mem_sets_of_nhdsWithin (hs : IsCompact s) {f : Filter X} (hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f) : sᶜ ∈ f :=
  by
  refine hs.compl_mem_sets fun x hx => ?_
  rcases hf x hx with ⟨t, ht, hst⟩
  replace ht := mem_inf_principal.1 ht
  apply mem_inf_of_inter ht hst
  rintro x ⟨h₁, h₂⟩ hs
  exact h₂ (h₁ hs)

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