English
A dependent version of Substructure.closure_induction. Given a property p and a closed under set of functions, the principle yields p for any element of closure L s.
Русский
Зависимая версия индукции closure. При наличии свойства p и замкнутости функций получаем выполнение p для каждого элемента closure L s.
LaTeX
$$$\forall s\subset M, \forall p, (Hs, Hfun) \Rightarrow \forall x\in closure L s, p x$$$
Lean4
/-- A dependent version of `Substructure.closure_induction`. -/
@[elab_as_elim]
theorem closure_induction' (s : Set M) {p : ∀ x, x ∈ closure L s → Prop}
(Hs : ∀ (x) (h : x ∈ s), p x (subset_closure h))
(Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f {x | ∃ hx, p x hx}) {x} (hx : x ∈ closure L s) : p x hx :=
by
refine Exists.elim ?_ fun (hx : x ∈ closure L s) (hc : p x hx) => hc
exact closure_induction hx (fun x hx => ⟨subset_closure hx, Hs x hx⟩) @Hfun
