isClosed_range_of_spaced_out — Mathlib

English

If a family f: ι → α is spaced out with respect to an entourage V0 ∈ 𝓤 α, then the range of f is closed.

Русский

Если множество значений функции f: ι → α разбросано по V0, то образ f (range f) замкнут.

LaTeX

$$$[T0Space(α)]\ V_0 \in 𝓤(α) \rightarrow \text{Pairwise}(x,y) \Rightarrow ... \Rightarrow\text{IsClosed}(\mathrm{range}(f))$$$

Lean4

theorem isClosed_range_of_spaced_out {ι} [T0Space α] {V₀ : Set (α × α)} (V₀_in : V₀ ∈ 𝓤 α) {f : ι → α}
    (hf : Pairwise fun x y => (f x, f y) ∉ V₀) : IsClosed (range f) :=
  isClosed_of_spaced_out V₀_in <| by
    rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ h
    exact hf (ne_of_apply_ne f h)

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