English
To prove a property of an element of the adic completion, it suffices to prove it for all Cauchy sequences via mk I M.
Русский
Чтобы доказать свойство для элемента адического завершения, достаточно доказать его для всех последовательностей Коши через отображение mk I M.
LaTeX
$$$\forall p:\mathrm{AdicCompletion}(I,M)\to\mathrm{Prop},\ \big(\forall f:\mathrm{AdicCauchySequence}(I,M),\ p(\mathrm{mk}\ I\ M\ f)\big) \Rightarrow \forall x:\mathrm{AdicCompletion}(I,M),\ p(x)$$$
Lean4
/-- To show a statement about an element of `adicCompletion I M`, it suffices to check it
on Cauchy sequences. -/
theorem induction_on {p : AdicCompletion I M → Prop} (x : AdicCompletion I M)
(h : ∀ (f : AdicCauchySequence I M), p (mk I M f)) : p x :=
by
obtain ⟨f, rfl⟩ := mk_surjective I M x
exact h f
