isClosed_iff' — Mathlib

English

For hf IsInducing, IsClosed s iff ∀ x, f x ∈ closure (f '' s) → x ∈ s.

Русский

Для hf IsInducing, s замкнуто тогда и только тогда, когда ∀ x, f x ∈ closure (f '' s) → x ∈ s.

LaTeX

$$$\operatorname{IsInducing}(f) \Rightarrow \forall s, \operatorname{IsClosed}(s) \iff \forall x, f(x) \in \operatorname{closure}(f''(s)) \Rightarrow x \in s.$$$

Lean4

theorem isClosed_iff' (hf : IsInducing f) {s : Set X} : IsClosed s ↔ ∀ x, f x ∈ closure (f '' s) → x ∈ s := by
  rw [hf.eq_induced, isClosed_induced_iff']

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