OAI/Geometry/Cannon/ScalarLimits/Exhaustion.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CannonDiagonal.select_strictMono_of_eventuallyline 24 - def
OAI.CannonDiagonal.exhaustionline 37 - lemma
OAI.CannonDiagonal.exhaustion_isCompactline 40 - lemma
OAI.CannonDiagonal.not_mem_exhaustionline 44 - lemma
OAI.CannonDiagonal.compact_eventually_subset_exhaustionline 49 - lemma
OAI.CannonDiagonal.enlarged_cells_eventually_subsetline 63 - theorem
OAI.CannonDiagonal.common_mesh_diagonalline 84