Mathlib Map

Theorems · Theorem · group theory

DoubleCoset.finite_quotient_iff_exists_finset_iUnion_eq_univ

∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G),
  Finite (DoubleCoset.Quotient ↑H ↑K) ↔ ∃ I, ⋃ i ∈ I, DoubleCoset.quotToDoubleCoset H K i = Set.univ
Defined in
Mathlib.GroupTheory.DoubleCoset
Cited by
0 results in Mathlib
Foundations
Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Group
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Set · cited by 53352SetFinset · cited by 13712FinsetSetLike.coe · cited by 8199SetLike.coeFintype · cited by 7736FintypeGroup · cited by 6238GroupSet.range · cited by 4705Set.rangeSet.univ · cited by 3945Set.univSubgroup · cited by 3593SubgroupFinset.univ · cited by 3473Finset.univFinite · cited by 3029FiniteSet.iUnion · cited by 2483Set.iUnionSet.Finite · cited by 1814Set.FiniteSet.iUnion_congr_Prop · cited by 374Set.iUnion_congr_Propnonempty_fintype · cited by 261nonempty_fintypeFinset.finite_toSet · cited by 210Finset.finite_toSetDoubleCoset.finite_quotient_i…CITED BYCITES

Cites21

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement and proof · cited by 53,352
  • Finsetstatement and proof · cited by 13,712
  • SetLike.coestatement and proof · cited by 8,199
  • Fintypeproof · cited by 7,736
  • Groupstatement and proof · cited by 6,238
  • Set.rangeproof · cited by 4,705
  • Set.univstatement and proof · cited by 3,945
  • Subgroupstatement and proof · cited by 3,593
  • Finset.univproof · cited by 3,473
  • Finitestatement and proof · cited by 3,029
  • Set.iUnionstatement and proof · cited by 2,483
  • Set.Finiteproof · cited by 1,814

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.