induction_on — Mathlib

English

Let e: α → β be a map with dense range. If the closed set {q ∈ β × β | p q.1 q.2} contains all pairs (e a1, e a2) then p(b1, b2) holds for all b1, b2.

Русский

Пусть e: α → β имеет плотное образующее. Если замкнутое множество {q ∈ β × β | p q1 q2} содержит все пары вида (e a1, e a2), то p(b1, b2) выполняется для всех b1, b2.

LaTeX

$$$$\forall b_1,b_2\, p(b_1,b_2)$$ under dense range and closure conditions (see above).$$

Lean4

@[elab_as_elim]
theorem induction_on [TopologicalSpace β] {e : α → β} (he : DenseRange e) {p : β → Prop} (b₀ : β)
    (hp : IsClosed {b | p b}) (ih : ∀ a : α, p <| e a) : p b₀ :=
  isClosed_property he hp ih b₀

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