ext — Mathlib

English

Two elements of AdicCompletion I M are equal if all their coordinates agree: x = y whenever x.val n = y.val n for all n.

Русский

Два элемента AdicCompletion I M равны тогда, когда во всех координатах совпадают: x = y, если x.val n = y.val n для всех n.

LaTeX

$$$ \\forall x,y \\in \\mathrm{AdicCompletion}(I,M), (\\forall n, x.val(n) = y.val(n)) \\Rightarrow x = y $$$

Lean4

@[ext]
theorem ext {x y : AdicCompletion I M} (h : ∀ n, x.val n = y.val n) : x = y :=
  Subtype.eq <| funext h

Похожие утверждения