English
Let e: α → β be dense. If the closed set {q ∈ β × β × β | p q.1 q.2.1 q.2.2} contains all triples (e a1, e a2, e a3), then p(b1, b2, b3) for all b1,b2,b3.
Русский
Пусть e: α → β имеет плотное образующее. Если множество {q ∈ β × β × β | p q1 q2 q3} замкнуто и содержит все тройки вида (e a1, e a₂, e a3), то p(b1,b2,b3) выполняется для всех b1,b2,b3.
LaTeX
$$$$\forall b_1,b_2,b_3\, p(b_1,b_2,b_3)$$ under dense range and closure conditions (see above).$$
Lean4
@[elab_as_elim]
theorem induction_on₂ [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₂ :=
isClosed_property2 he hp h _ _
