Miikka Koskinen miikka
miikka
/ orbital.py
Created
May 17, 2016 16:35
— forked from jkseppan/orbital.py
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| from collections import defaultdict, namedtuple | |
| import numpy as np | |
| def visible_cap_central_angle(altitude): | |
| earth_radius = 6371.0 | |
| return np.arctan2(np.sqrt(altitude * (altitude + 2 * earth_radius)), | |
| earth_radius) | |
| def hav(x): | |
| return np.sin(x/2)**2 |
miikka
/ topology.v
Created
January 15, 2016 10:25
— forked from andrejbauer/topology.v
How to get started with point-set topology in Coq. This is not actually how one would do it, but it is an intuitive setup for a classical mathematician.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* How do to topology in Coq if you are secretly an HOL fan. | |
| We will not use type classes or canonical structures because they | |
| count as "advanced" technology. But we will use notations. | |
| *) | |
| (* We think of subsets as propositional functions. | |
| Thus, if [A] is a type [x : A] and [U] is a subset of [A], | |
| [U x] means "[x] is an element of [U]". | |
| *) | |
| Definition P (A : Type) := A -> Prop. |