ext — Mathlib

English

Extensionality principle: filtrations are equal if their index-wise σ-algebras coincide.

Русский

Принцип экстенсиональности: фильтрации равны, если их сигма-алгебры на каждом индексе совпадают.

LaTeX

$$$\\mathrm{ext}(f,g) \\,:\\, (f.seq = g.seq) \\Rightarrow f = g$$$

Lean4

@[ext]
protected theorem ext {f g : Filtration ι m} (h : (f : ι → MeasurableSpace Ω) = g) : f = g := by cases f; cases g; congr

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