ext — Mathlib

English

Two Dynkin systems are equal if they have the same members on every subset; equivalently, if for all s, Has₁ s ↔ Has₂ s, then the two Dynkin systems are equal.

Русский

Две Dynkin-системы равны тогда и только тогда, когда на каждом множестве они совпадают: если для всех s поддержка Has одинакова, то системы равны.

LaTeX

$$$\forall s \subseteq α, d_1.Has s \iff d_2.Has s \Rightarrow d_1 = d_2$$$

Lean4

@[ext]
theorem ext : ∀ {d₁ d₂ : DynkinSystem α}, (∀ s : Set α, d₁.Has s ↔ d₂.Has s) → d₁ = d₂
  | ⟨s₁, _, _, _⟩, ⟨s₂, _, _, _⟩, h =>
    by
    have : s₁ = s₂ := funext fun x => propext <| h x
    subst this
    rfl

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