isClosed_iff — Mathlib

English

If hf is IsInducing, then a set s ⊆ X is closed iff there exists t closed in Y with f⁻¹'t = s.

Русский

Если hf — IsInducing, то множество s закрыто тогда и только тогда, когда существует множество t, замкнутое в Y, такое что f⁻¹'(t) = s.

LaTeX

$$$\operatorname{IsInducing}(f) \Rightarrow \forall s, \operatorname{IsClosed}(s) \iff \exists t, \operatorname{IsClosed}(t) \land f^{-1}(t) = s.$$$

Lean4

theorem isClosed_iff (hf : IsInducing f) {s : Set X} : IsClosed s ↔ ∃ t, IsClosed t ∧ f ⁻¹' t = s := by
  rw [hf.eq_induced, isClosed_induced_iff]

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