Theorems · Theorem · category theory

Profinite.NobelingProof.one_sub_e_mem_of_false

∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] (s : Finset I)
  {x y : ↑(Profinite.NobelingProof.π C fun x => x ∈ s)} {a : I},
  ↑y a = true →
    ↑x a = false →
      1 - Profinite.NobelingProof.e (Profinite.NobelingProof.π C fun x => x ∈ s) a ∈
        Profinite.NobelingProof.factors C s x

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.Span

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrder