definition A.76 Star-shaped set
open in the book ·
appendices/A-long-proofs.tex:4927
· p. 2831
- ground object -- no derivation owed
Rests on
-
depends_on
definition 6.26
Open ball; metric topology
¶
-
depends_on
definition 6.24
Metric
¶
- depends_on definition 3.43 Map ¶
- depends_on definition 3.38 Ordered pair and Cartesian product ¶
-
depends_on
definition 6.2
Open set
¶
-
depends_on
definition 6.1
Topological space
¶
- depends_on definition 3.31 Empty set ¶
-
depends_on
definition 3.35
Union, intersection, difference
¶
- depends_on definition 3.8 Conjunction ¶
- depends_on definition 3.9 Disjunction ¶
- depends_on definition 3.7 Negation ¶
- depends_on definition 3.30 Subset ¶
- depends_on equation 3.51 eq:set-indexed ¶
-
depends_on
definition 6.1
Topological space
¶
- depends_on definition 6.1 Topological space ¶ ↺
-
depends_on
definition 6.24
Metric
¶
Supports
- depends_on lemma A.77 Poincaré lemma, converse form ¶
Neighborhood
Every logical edge within two steps of this node.
- declared and complete
- partly declared
- a check failed
- not graded
- declared in the source
- inferred from structure
Edges
| type | direction | node | provenance | where |
|---|---|---|---|---|
depends_on |
→ | Open ball; metric topology | declared | appendices/A-long-proofs.tex:4931 |
depends_on |
← | Poincaré lemma, converse form | declared | appendices/A-long-proofs.tex:4947 |