OAI/Topology/ArtinGroups/Coxeter/WeakPrefix.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.CoxeterExchange.WeakPrefix line 10
2. lemma OAI.HarmonicArtin.CoxeterExchange.weakPrefix_one line 12
3. lemma OAI.HarmonicArtin.CoxeterExchange.weakPrefix_refl line 13
4. lemma OAI.HarmonicArtin.CoxeterExchange.weakPrefix_length line 14
5. lemma OAI.HarmonicArtin.CoxeterExchange.weakPrefix_suffix line 16
6. lemma OAI.HarmonicArtin.CoxeterExchange.weakPrefix_trans line 19
7. lemma OAI.HarmonicArtin.CoxeterExchange.weakPrefix_antisymm line 28
8. lemma OAI.HarmonicArtin.CoxeterExchange.weakPrefix_eq_of_length line 33
9. lemma OAI.HarmonicArtin.CoxeterExchange.weakPrefix_simple_iff line 37
10. lemma OAI.HarmonicArtin.CoxeterExchange.weakPrefix_left_remove line 41
11. lemma OAI.HarmonicArtin.CoxeterExchange.weakPrefix_left_add line 51
12. lemma OAI.HarmonicArtin.CoxeterExchange.exists_simple_prefix line 67
13. lemma OAI.HarmonicArtin.CoxeterExchange.weakPrefix_first_of_reduced line 78
14. lemma OAI.HarmonicArtin.CoxeterExchange.simple_pair_prefix line 88