ext' — Mathlib

English

Equality of two elements x,y ∈ M F is determined by the equality of their approximations at every level: if x.approx i = y.approx i for all i, then x = y.

Русский

Равенство двух элементов x,y из M F определяется по равенству их аппроксимаций на каждом уровне: если x.approx i = y.approx i для всех i, то x = y.

LaTeX

$$$\\forall (F:\\text{PFunctor})\\ (x,y:\\, M F),\\; (\\forall i:\\, \\mathbb{N},\\; x.approx i = y.approx i)\\;\\Rightarrow\\; x = y$$$

Lean4

theorem ext' (x y : M F) (H : ∀ i : ℕ, x.approx i = y.approx i) : x = y :=
  by
  cases x
  cases y
  congr with n
  apply H

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