Theorems · Definition · algebraic topology

IsAddQuotientCoveringMap.casesOn

{E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {f : E → X} →
          {G : Type u_4} →
            [inst_2 : AddGroup G] →
              [inst_3 : AddAction G E] →
                {motive : IsAddQuotientCoveringMap f G → Sort u} →
                  (t : IsAddQuotientCoveringMap f G) →
                    ((toIsQuotientMap : Topology.IsQuotientMap f) →
                        (toContinuousConstVAdd : ContinuousConstVAdd G E) →
                          (apply_eq_iff_mem_orbit : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) →
                            (disjoint :
                                ∀ (e : E), ∃ U ∈ nhds e, ∀ (g : G), ((fun x => g +ᵥ x) '' U ∩ U).Nonempty → g = 0) →
                              motive ⋯) →
                      motive t

Defined in

Mathlib.Topology.Covering.Quotient

Cited by

1 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceAddGroupAddAction