mem_wf — Mathlib

English

The relation ∈ on Class is well-founded.

Русский

Отношение принадлежности на классе является хорошо основанным.

LaTeX

$$$\\\\mathrm{WellFounded} \\\\mathrm{Class} \\\\left( \\\\in \\\\right).$$$

Lean4

theorem mem_wf : @WellFounded Class.{u} (· ∈ ·) :=
  ⟨by
    have H : ∀ x : ZFSet.{u}, @Acc Class.{u} (· ∈ ·) ↑x :=
      by
      refine fun a => ZFSet.inductionOn a fun x IH => ⟨_, ?_⟩
      rintro A ⟨z, rfl, hz⟩
      exact IH z hz
    refine fun A => ⟨A, ?_⟩
    rintro B ⟨x, rfl, _⟩
    exact H x⟩

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