pi_ext_iff — Mathlib

English

The ext lemma specialized to finite index sets states that f=g if they agree on all Pi.single i x; this is a variant of pi_ext with finite ι.

Русский

Специализация экст-леммы для конечного множества индексов: если они согласованы на всех Pi.single i x, то f=g.

LaTeX

$$$\\forall i,\\; f(\\Pi.single i x) = g(\\Pi.single i x) \\implies f=g.$$$

Lean4

theorem pi_ext_iff : f = g ↔ ∀ i x, f (Pi.single i x) = g (Pi.single i x) :=
  ⟨fun h _ _ => h ▸ rfl, pi_ext⟩

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