isOpen_iff — Mathlib

English

Duplicate of isOpen_iff; IsOpen s iff there exists t open with f⁻¹'(t) = s.

Русский

Дублирует isOpen_iff; IsOpen s эквивалентно существованию открытого множества t с f⁻¹'(t) = s.

LaTeX

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

Lean4

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

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