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