OAI/Topology/ArtinGroups/Realizations/WeightInclusion.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.HarmonicArtin.weightInclusionline 14 - def
OAI.HarmonicArtin.weightRestrictline 16 - lemma
OAI.HarmonicArtin.weightRestrict_applyline 29 - lemma
OAI.HarmonicArtin.weightRestrict_mapline 32 - lemma
OAI.HarmonicArtin.weight_le_oneline 46 - def
OAI.HarmonicArtin.weightTimeline 53 - def
OAI.HarmonicArtin.weightVertexline 55 - lemma
OAI.HarmonicArtin.coneWeights_one_vertexline 65 - lemma
OAI.HarmonicArtin.weight_eq_vertex_of_oneline 70 - def
OAI.HarmonicArtin.weightDeleteline 90 - lemma
OAI.HarmonicArtin.weightDelete_applyline 119 - lemma
OAI.HarmonicArtin.weightDelete_supportline 123