Theorem exterior_union

Modification history

2024-09-24 06:31

Mathlib/Topology/AlexandrovDiscrete.lean

chore(AlexandrovDiscrete): move `exterior` to new files (#16957) …

Modified exterior_union View on Github →

2024-09-19 18:37

Mathlib/Topology/AlexandrovDiscrete.lean

feat(Topology/AlexandrovDiscrete): generalize some lemmas (#16932) …

Modified exterior_union View on Github →

2023-09-14 10:14

Mathlib/Topology/AlexandrovDiscrete.lean

feat: Exterior of a set (#6982) …

Added exterior_union View on Github →