range_Iic — Mathlib

English

The Iic range provides a countable separating family on s.

Русский

Диапазон Iic образует счётно разделяющее семейство на s.

LaTeX

$$$ HasCountableSeparatingOn X (\cdot \in range Iic) s $$$

Lean4

instance range_Iic : HasCountableSeparatingOn X (· ∈ range Iic) s :=
  let ⟨t, htc, ht_sub, ht⟩ := (range_Ioi (X := X) (s := s)).1
  ⟨compl '' t, htc.image _, by simpa [← compl_inj_iff (x := Ioi _)] using ht_sub, by simpa [not_iff_not]⟩

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