OAI/Analysis/Commutator/WordTopology2.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Kadison.Topology.exists_stage_piline 20 - lemma
OAI.Kadison.Topology.dense_iUnion_piline 30 - lemma
OAI.Kadison.Topology.dense_iUnion_prodline 39