English
An induction principle for open sets: if the basis B supports an induction step for basis elements and unions, then every open set satisfies property P.
Русский
Индукционное свойство для открытых множеств: если база B поддерживает индуктивное переходо для базисных элементов и объединений, то любое открытое множество обладает свойством P.
LaTeX
$$isOpen_induction {P : Set α → Prop} (hB : IsTopologicalBasis B) (basis : ∀ b ∈ B, P b) (sUnion : ∀ S, (∀ s ∈ S, P s) → P (⋃₀ S)) {s : Set α} (hs : IsOpen s) : P s$$
Lean4
@[elab_as_elim]
theorem isOpen_induction {P : Set α → Prop} (hB : IsTopologicalBasis B) (basis : ∀ b ∈ B, P b)
(sUnion : ∀ S, (∀ s ∈ S, P s) → P (⋃₀ S)) {s : Set α} (hs : IsOpen s) : P s := by
obtain ⟨S, hS, rfl⟩ := hB.open_eq_sUnion hs; exact sUnion _ fun b hb ↦ basis _ <| hS hb
