English
Induction principle on Completion α × Completion β × Completion γ: if a predicate p on the triple is closed and holds on all coe a, coe b, coe c, then it holds for all triples.
Русский
Принцип индукции на Completion α × Completion β × Completion γ: если p замкнуто и выполняется на всех тройках coe a, coe b, coe c, то выполняется на всех тройках.
LaTeX
$$$\\text{IsClosed}(\\{x:\\mathrm{Completion}(\\alpha) \\times \\mathrm{Completion}(\\beta) \\times \\mathrm{Completion}(\\gamma) \\mid p(x.1,x.2.1,x.2.2)\\}) \\land \\forall a:\\alpha,\\forall b:\\beta,\\forall c:\\gamma,\\ p(\\mathrm{coe}'a, \\mathrm{coe}'b, \\mathrm{coe}'c) \\Rightarrow \\forall x:\\mathrm{Completion}(\\alpha) \\times \\mathrm{Completion}(\\beta) \\times \\mathrm{Completion}(\\gamma),\\ p(x.1,x.2.1,x.2.2)$$$
Lean4
@[elab_as_elim]
theorem induction_on₃ {p : Completion α → Completion β → Completion γ → Prop} (a : Completion α) (b : Completion β)
(c : Completion γ) (hp : IsClosed {x : Completion α × Completion β × Completion γ | p x.1 x.2.1 x.2.2})
(ih : ∀ (a : α) (b : β) (c : γ), p a b c) : p a b c :=
have : ∀ x : Completion α × Completion β × Completion γ, p x.1 x.2.1 x.2.2 :=
isClosed_property denseRange_coe₃ hp fun ⟨a, b, c⟩ => ih a b c
this (a, b, c)
