English
For f: α → β, a ∈ α, s ⊆ α, a ∈ closure(s) in the induced topology by f if and only if f(a) ∈ closure(f''s).
Русский
Для отображения f: α → β, точки a ∈ α, и подмножества s ⊆ α: a ∈ замыкания s в индуцированной топологии тогда и только тогда, когда f(a) ∈ closure( f''s ).
LaTeX
$$$a \\in {\\mathrm{closure}}(s) \\text{ in } (\\alpha, \\mathrm{induced} f) \\iff f(a) \\in \\mathrm{closure}(f''s).$$$
Lean4
theorem closure_induced {f : α → β} {a : α} {s : Set α} : a ∈ @closure α (t.induced f) s ↔ f a ∈ closure (f '' s) := by
simp only [mem_closure_iff_frequently, nhds_induced, frequently_comap, mem_image, and_comm]
