OAI/Analysis/Pureness/Completion/ClosedIdeals.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.CuntzPureness.TopologicallySimpleline 10 - def
OAI.CuntzPureness.closedTwoSidedIdealline 13 - theorem
OAI.CuntzPureness.coe_closedTwoSidedIdealline 38 - theorem
OAI.CuntzPureness.closure_span_singleton_eq_univline 42