Theorems · Theorem · algebraic topology

Topology.IsQuotientMap.trivializationOfSMulDisjoint_source

∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hf : Topology.IsQuotientMap f) [inst_4 : ContinuousConstSMul G E]
  (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) [inst_5 : TopologicalSpace G]
  [inst_6 : DiscreteTopology G] (U : Set E) (open_U : IsOpen U)
  (disjoint : ∀ (g : G), ((fun x => g • x) '' U ∩ U).Nonempty → g = 1),
  (hf.trivializationOfSMulDisjoint hfG U open_U disjoint).source = f ⁻¹' f '' U

Defined in

Mathlib.Topology.Covering.Quotient

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceGroupMulActionContinuousConstSMulTopologicalSpaceDiscreteTopology