unique — Mathlib

English

Let f: β → α where α is a topological commutative monoid and L is a summation filter. If HasProd f a1 L and HasProd f a2 L hold, then a1 = a2.

Русский

Пусть f: β → α, где α — топологическая коммутативная моноида, и L — суммирующий фильтр. Если выполняются HasProd f a1 L и HasProd f a2 L, то a1 = a2.

LaTeX

$$$\forall a_1,a_2 \in \alpha,\ HasProd(f,a_1,L) \to HasProd(f,a_2,L) \to a_1 = a_2$$$

Lean4

@[to_additive]
theorem unique {a₁ a₂ : α} : HasProd f a₁ L → HasProd f a₂ L → a₁ = a₂ := by classical exact tendsto_nhds_unique

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