induction_on₃ — Mathlib

English

If e: α → β has dense range and p is closed, and p(e(a)) holds for all a, then p(b0) holds for any b0 ∈ β.

Русский

Пусть e: α → β имеет плотное образующее. Пусть множество {x ∈ β | p(x)} замкнуто и p(e(a)) выполняется для всех a. Тогда p(b0) выполняется для любого b0 ∈ β.

LaTeX

$$$$\operatorname{DenseRange}(e) \Rightarrow \forall b_0\, p(b_0)$$ under (hp closed) and (ih).$$

Lean4

@[elab_as_elim]
theorem induction_on₃ [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₃ :=
  isClosed_property3 he hp h _ _ _

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