OAI/Topology/ArtinGroups/Realizations/RestrictedCellEmbedding.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.HarmonicArtin.restrictedCellEmbeddingline 14 - lemma
OAI.HarmonicArtin.restrictedCellEmbedding_fullline 28 - lemma
OAI.HarmonicArtin.restrictedCellEmbedding_full_preimageline 38 - lemma
OAI.HarmonicArtin.restrictedCellEmbedding_topline 55 - lemma
OAI.HarmonicArtin.lifted_same_top_type_uniqueline 64