English
If e: α → β has dense range and the set {x ∈ β | p(x)} is closed, and p(e(a)) holds for every a ∈ α, then p(b) holds for all b ∈ β.
Русский
Пусть e: α → β имеет плотное образующее множество и множество {x ∈ β | p(x)} замкнуто, а p(e(a)) выполняется для всех a ∈ α. Тогда p(b) выполняется для всех b ∈ β.
LaTeX
$$$$\operatorname{DenseRange}(e) \wedge \operatorname{IsClosed}\bigl\{x \in \beta \mid p(x)\bigr\} \wedge (\forall a, p(e(a))) \Longrightarrow (\forall b, p(b)).$$$$
Lean4
theorem isClosed_property [TopologicalSpace β] {e : α → β} {p : β → Prop} (he : DenseRange e) (hp : IsClosed {x | p x})
(h : ∀ a, p (e a)) : ∀ b, p b :=
by
have : univ ⊆ {b | p b} :=
calc
univ = closure (range e) := he.closure_range.symm
_ ⊆ closure {b | p b} := (closure_mono <| range_subset_iff.mpr h)
_ = _ := hp.closure_eq
simpa only [univ_subset_iff, eq_univ_iff_forall, mem_setOf]
