English
Let e: α → β have dense range, and the closed set {q ∈ β × β | p(q1, q2)}. If p(e(a1), e(a2)) holds for all a1, a2, then p(b1, b2) holds for all b1, b2.
Русский
Пусть e: α → β имеет плотное образующее множество, множество {q ∈ β × β | p(q1, q2)} замкнуто, и p(e(a1), e(a2)) выполняется для всех a1, a2. Тогда p(b1, b2) выполняется для всех b1, b2.
LaTeX
$$$$\operatorname{DenseRange}(e) \rightarrow \operatorname{IsClosed}\bigl\{q = (q_1,q_2) \mid p(q_1,q_2)\bigr\} \rightarrow \bigl(\forall a_1,a_2,\ p( e(a_1), e(a_2) )\bigr) \Rightarrow (\forall b_1,b_2,\ p(b_1,b_2)).$$$$
Lean4
theorem isClosed_property2 [TopologicalSpace β] {e : α → β} {p : β → β → Prop} (he : DenseRange e)
(hp : IsClosed {q : β × β | p q.1 q.2}) (h : ∀ a₁ a₂, p (e a₁) (e a₂)) : ∀ b₁ b₂, p b₁ b₂ :=
have : ∀ q : β × β, p q.1 q.2 := isClosed_property (he.prodMap he) hp fun _ => h _ _
fun b₁ b₂ => this ⟨b₁, b₂⟩
