Theorems · Theorem · category theory

Profinite.NobelingProof.C0.congr_simp

∀ {I : Type u} (C C_1 : Set (I → Bool)),
  C = C_1 →
    ∀ [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o o_1 : Ordinal.{u}} (e_o : o = o_1)
      (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (a a_1 : I → Bool),
      a = a_1 → Profinite.NobelingProof.C0 C ho a = Profinite.NobelingProof.C0 C_1 ⋯ a_1

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.Successor

Cited by

0 results in Mathlib

Foundations

Depth 39 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderWellFoundedLT