| Tue, 05 Mar 2013 15:43:19 +0100 | hoelzl | move lemma Inf to usage point | changeset | files |
| Tue, 05 Mar 2013 15:43:18 +0100 | hoelzl | tuned proof of Edelstein fixed point theorem (use continuity of dist and attains_sup) | changeset | files |
| Tue, 05 Mar 2013 15:43:17 +0100 | hoelzl | tuned proofs (used continuity of infdist, dist and continuous_attains_sup) | changeset | files |
| Tue, 05 Mar 2013 15:43:16 +0100 | hoelzl | generalized continuous/compact_attains_inf/sup from real to linorder_topology | changeset | files |
| Tue, 05 Mar 2013 15:43:15 +0100 | hoelzl | continuity of pair operations | changeset | files |
| Tue, 05 Mar 2013 15:43:14 +0100 | hoelzl | use generate_topology for second countable topologies, does not require intersection stable basis | changeset | files |