FLT/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Total boundedness for topological groups with small finite-index subgroups

Material destined for Mathlib.

Imports (2)
Imported by 3 files
  1. lemma IsTopologicalGroup.totallyBounded line 19 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Group, TopologicalSpace, IsTopologicalGroup, Set, Membership.mem, Filter, nhds, OfNat.ofNat, Exists, Subgroup, And, Subgroup.FiniteIndex, LE.le, TotallyBounded, IsTopologicalGroup.rightUniformSpace, Set.univ

    Proof uses: UniformSpace, Prod, uniformity, Set.preimage, HMul.hMul, Prod.snd, Inv.inv, Prod.fst, Set.Finite, Set.iUnion, Set.ofPred, Prod.mk, Finite, HasQuotient.Quotient, MulOpposite, Subgroup.op, Exists.intro, Set.range, Function.comp, MulOpposite.unop and 25 more

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

    Open to load the checked before-and-after goal states.