ext — Mathlib

English

An Extensional principle for AdicCauchySequence: equality is determined by coordinates.

Русский

Принцип экстенсиональности для AdicCauchySequence: равенство определяется координатами.

LaTeX

$$$ \\forall x,y:\\mathrm{AdicCauchySequence}(I,M), (\\forall n, x(n) = y(n)) \\Rightarrow x = y $$$

Lean4

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

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