isClosed_induced_iff' — Mathlib

English

For any f: α → β and s ⊆ α, IsClosed of s in the induced topology t.induced f is equivalent to: for all a, f(a) ∈ closure(f''s) implies a ∈ s.

Русский

Для отображения f: α → β и подмножества s ⊆ α: IsClosed в индуцированной топологии эквивалентно условию: ∀ a, f(a) ∈ closure(f''s) → a ∈ s.

LaTeX

$$$IsClosed[t.induced f] s \\iff \\forall a,\\; f a \\in \\mathrm{closure}(f'' s) \\to a \\in s.$$$

Lean4

theorem isClosed_induced_iff' {f : α → β} {s : Set α} : IsClosed[t.induced f] s ↔ ∀ a, f a ∈ closure (f '' s) → a ∈ s :=
  by simp only [← closure_subset_iff_isClosed, subset_def, closure_induced]

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