English
Let e: α → β have dense range. If the closed set {q ∈ β × β × β | p(q.1, q.2.1, q.2.2)} contains all triples (e a1, e a2, e a3), then it contains all triples in β.
Русский
Пусть e: α → β имеет плотное образующее множество. Если множество {q ∈ β × β × β | p(q.1, q.2.1, q.2.2)} замкнуто и содержит все тройки вида (e a1, e a2, e a3), тогда оно содержит все тройки в β.
LaTeX
$$$$\operatorname{DenseRange}(e) \rightarrow \operatorname{IsClosed}\bigl\{q=(q_1,q_2,q_3)\mid p(q_1,q_2,q_3)\bigr\} \rightarrow \bigl(\forall a_1,a_2,a_3,\ p( e(a_1), e(a_2), e(a_3))\bigr) \Rightarrow (\forall b_1,b_2,b_3,\ p(b_1,b_2,b_3)).$$$$
Lean4
theorem isClosed_property3 [TopologicalSpace β] {e : α → β} {p : β → β → β → Prop} (he : DenseRange e)
(hp : IsClosed {q : β × β × β | p q.1 q.2.1 q.2.2}) (h : ∀ a₁ a₂ a₃, p (e a₁) (e a₂) (e a₃)) :
∀ b₁ b₂ b₃, p b₁ b₂ b₃ :=
have : ∀ q : β × β × β, p q.1 q.2.1 q.2.2 := isClosed_property (he.prodMap <| he.prodMap he) hp fun _ => h _ _ _
fun b₁ b₂ b₃ => this ⟨b₁, b₂, b₃⟩
