Hypertopology.lean`

Explanation legend

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

25 declarations, 0 contain sorry, 0 axioms

Hypertopology

[FRAME] Finite topological interpretation of recursive nearness.

This is the Lean port of the local hypertopology candidate. It carries the finite topology frame and the properties that frame establishes, and nothing more.

What is proved here is finite and mechanical. A topology over a carrier of known size is a list of open sets; the axioms that matter are that the empty set and the whole carrier are open, that the opens are closed under union and intersection, and that closure, interior, and boundary are the operations the frame defines. Those are decidable over a finite carrier, so the compiler checks them.

The carrier's size is a type parameter rather than a field. A Fin n whose n is a structure field cannot be given a literal point, because the elaborator cannot reduce the field to a numeral at that point. Making the size a parameter means each topology is a type-level choice, and the numerals are ordinary literals.

What is not proved here, and cannot be, is any claim that nearness has a topological nature in general. The frame is a finite carrier with a chosen collection of opens. It does not say that recursive nearness is continuous, and it does not say that the finite models here are the intended ones. The Python source carries the same [FRAME] classification, and this port keeps it: a finite consistency result is not a foundation.

Imports (2)

Imported by 1 file

Hyperfields/AllFields.lean

structure Hyperfields.Fields.Hypertopology.FiniteTopology A finite topology over a fixed carrier line 52 source
A finite topology over a carrier of n points.
The carrier is Fin n, so the number of points is fixed by the type rather than checked at runtime, and every point is a decidable value. The opens are a list of carrier subsets; wellShaped is where the axioms are checked.

The carrier's size is part of its type, so a topology is a finite list of opens over a known number of points.

no axioms what this means
Statement uses: Nat
```
structure FiniteTopology (n : Nat) where
…
```
def Hyperfields.Fields.Hypertopology.FiniteTopology.wellShaped The axioms a finite topology must satisfy line 70 source
Whether the opens satisfy the topology axioms.
The three axioms are checked here rather than assumed:
1. The empty set is open.
2. The whole carrier is open.
3. The opens are closed under union and intersection.
The checks are decidable because the carrier is finite and its equality is decidable.
A topology is empty set, whole carrier, and closure under the two lattice operations; a frame that drops any of these is not a topology.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hypertopology.FiniteTopology, Bool
Proof uses: List, Fin, Hyperfields.Finite.carrier, Hyperfields.Finite.finLe, Bool.and, Hyperfields.Finite.mem, List.nil, Hyperfields.Fields.Hypertopology.FiniteTopology.opens, List.all, Hyperfields.Finite.union, Hyperfields.Finite.inter
5 instances, coercions and auxiliary constants left out.
```
def FiniteTopology.wellShaped {n : Nat} (topology : FiniteTopology n) : Bool :=
…
```
Mentions: Hyperfields.Fields.Hypertopology.FiniteTopology
def Hyperfields.Fields.Hypertopology.FiniteTopology.closure The closure of a subset line 94 source
The closure of a subset: the intersection of every closed superset of it.
A closed superset of subset is the complement of an open set that contains subset. The closure is therefore the intersection of all such complements, which is exactly the definition on a finite carrier.

Closure is the intersection of every closed superset of the subset, and on a finite carrier that intersection is computable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hypertopology.FiniteTopology, List, Fin
Proof uses: Hyperfields.Finite.carrier, Bool, Hyperfields.Finite.finLe, List.foldl, Hyperfields.Finite.diff, ite, Eq, Hyperfields.Finite.subset, Bool.true, Hyperfields.Finite.inter, Hyperfields.Fields.Hypertopology.FiniteTopology.opens
5 instances, coercions and auxiliary constants left out.
```
def FiniteTopology.closure {n : Nat} (topology : FiniteTopology n)
    (candidate : List (Fin n)) : List (Fin n) :=
…
```
Mentions: Hyperfields.Fields.Hypertopology.FiniteTopology
def Hyperfields.Fields.Hypertopology.FiniteTopology.interior The interior of a subset line 107 source
The interior of a subset: the union of every open set contained in it.

Interior is the union of every open set contained in the subset, which is the largest open set inside it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hypertopology.FiniteTopology, List, Fin
Proof uses: Bool, Hyperfields.Finite.finLe, List.foldl, ite, Eq, Hyperfields.Finite.subset, Bool.true, Hyperfields.Finite.union, List.nil, Hyperfields.Fields.Hypertopology.FiniteTopology.opens
5 instances, coercions and auxiliary constants left out.
```
def FiniteTopology.interior {n : Nat} (topology : FiniteTopology n)
    (candidate : List (Fin n)) : List (Fin n) :=
…
```
Mentions: Hyperfields.Fields.Hypertopology.FiniteTopology
def Hyperfields.Fields.Hypertopology.FiniteTopology.boundary The boundary of a subset line 119 source
The boundary of a subset: the intersection of its closure with the closure of its complement.

The boundary is where the closure and the closure of the complement meet, so it is the set of points that cannot be avoided on either side.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hypertopology.FiniteTopology, List, Fin
Proof uses: Hyperfields.Finite.carrier, Bool, Hyperfields.Finite.finLe, Hyperfields.Finite.inter, Hyperfields.Fields.Hypertopology.FiniteTopology.closure, Hyperfields.Finite.diff
4 instances, coercions and auxiliary constants left out.
```
def FiniteTopology.boundary {n : Nat} (topology : FiniteTopology n)
    (candidate : List (Fin n)) : List (Fin n) :=
…
```
Mentions: Hyperfields.Fields.Hypertopology.FiniteTopology
def Hyperfields.Fields.Hypertopology.continuousBetween Continuity of a map between finite topologies line 134 source
Whether a map between two finite topologies is continuous.
The map is given as a list of pairs, one per source point, and must be total and single valued. Continuity is checked by pulling back every open set of the target and asking whether the result is open in the source.

A map is continuous when the inverse image of every open set is open, which is decidable over a finite carrier.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hypertopology.FiniteTopology, List, Prod, Fin, Bool
Proof uses: Hyperfields.Finite.carrier, Bool.and, BEq.beq, List.length, List.all, Hyperfields.Finite.mem, Prod.fst, Prod.snd, List.eraseDups, List.map, Hyperfields.Fields.Hypertopology.FiniteTopology.opens, List.filter
7 instances, coercions and auxiliary constants left out.
```
def continuousBetween {m n : Nat}
    (source : FiniteTopology m) (target : FiniteTopology n)
    (mapping : List (Fin m × Fin n)) : Bool :=
…
```
Mentions: Hyperfields.Fields.Hypertopology.FiniteTopology
def Hyperfields.Fields.Hypertopology.discreteTwo The discrete topology on two points line 155 source
The discrete topology on two points: every subset is open.

Every subset is open, which is the finest possible topology and the strictest test of continuity.

standard axioms: propext what this means
Statement uses: Hyperfields.Fields.Hypertopology.FiniteTopology, OfNat.ofNat, Nat
Proof uses: Hyperfields.Fields.Hypertopology.FiniteTopology.mk, List.cons, List, Fin, List.nil
4 instances, coercions and auxiliary constants left out.
```
def discreteTwo : FiniteTopology 2 where
…
```
Mentions: Hyperfields.Fields.Hypertopology.FiniteTopology
def Hyperfields.Fields.Hypertopology.indiscreteTwo The indiscrete topology on two points line 161 source
The indiscrete topology on two points: only the empty set and the whole carrier are open.

Only the empty set and the whole carrier are open, which is the coarsest possible topology.

standard axioms: propext what this means
Statement uses: Hyperfields.Fields.Hypertopology.FiniteTopology, OfNat.ofNat, Nat
Proof uses: Hyperfields.Fields.Hypertopology.FiniteTopology.mk, List.cons, List, Fin, List.nil
4 instances, coercions and auxiliary constants left out.
```
def indiscreteTwo : FiniteTopology 2 where
…
```
Mentions: Hyperfields.Fields.Hypertopology.FiniteTopology
def Hyperfields.Fields.Hypertopology.chainTopology A three-point topology line 173 source
A concrete three-point topology used to check the axioms and the operations.
The carrier is {0, 1, 2} and the opens are ∅, {0}, {0, 1}, and the whole carrier. This is the finite chain topology, and every property below is checked by the compiler rather than asserted.

A concrete frame lets the compiler check the axioms and the operations against something a reader can see.

standard axioms: propext what this means
Statement uses: Hyperfields.Fields.Hypertopology.FiniteTopology, OfNat.ofNat, Nat
Proof uses: Hyperfields.Fields.Hypertopology.FiniteTopology.mk, List.cons, List, Fin, List.nil
4 instances, coercions and auxiliary constants left out.
```
def chainTopology : FiniteTopology 3 where
…
```
Mentions: Hyperfields.Fields.Hypertopology.FiniteTopology
theorem Hyperfields.Fields.Hypertopology.chain_topology_is_well_shaped The chain topology satisfies the axioms line 184 source
The three-point chain topology satisfies the topology axioms.

The concrete example must actually clear the axioms the frame demands, or the example proves nothing.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hypertopology.FiniteTopology.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hypertopology.chainTopology, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
3 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 185
  before
```
⊢ chainTopology.wellShaped = true
```
  after
  no goals remain
```
theorem chain_topology_is_well_shaped : chainTopology.wellShaped = true := by
…
```
theorem Hyperfields.Fields.Hypertopology.discrete_two_is_well_shaped The discrete topology satisfies the axioms line 190 source
The discrete two-point topology satisfies the topology axioms.

The concrete example must clear the axioms it is used to test.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hypertopology.FiniteTopology.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hypertopology.discreteTwo, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
3 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 191
  before
```
⊢ discreteTwo.wellShaped = true
```
  after
  no goals remain
```
theorem discrete_two_is_well_shaped : discreteTwo.wellShaped = true := by
…
```
theorem Hyperfields.Fields.Hypertopology.indiscrete_two_is_well_shaped The indiscrete topology satisfies the axioms line 196 source
The indiscrete two-point topology satisfies the topology axioms.

The coarsest possible topology still satisfies the axioms, which is the check that the axioms are not too strong.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hypertopology.FiniteTopology.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hypertopology.indiscreteTwo, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
3 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 197
  before
```
⊢ indiscreteTwo.wellShaped = true
```
  after
  no goals remain
```
theorem indiscrete_two_is_well_shaped : indiscreteTwo.wellShaped = true := by
…
```
theorem Hyperfields.Fields.Hypertopology.chain_closure_of_open The closure of the open set {0, 1} line 210 source
The closure of {0, 1} in the chain topology is the whole carrier.
This is the case that a hand-written intuition gets wrong. The set {0, 1} is open, but it is not closed: the only closed set that contains it is {0, 1, 2} itself. Closure is the intersection of the closed supersets, not the smallest closed set equal to the argument, so the closure is the whole carrier. The compiler checks this against the definition.

Closure is the intersection of the closed supersets, and on a chain the only closed superset of `{0, 1}` is the whole carrier.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, List, Fin, OfNat.ofNat, Nat, Hyperfields.Fields.Hypertopology.FiniteTopology.closure, Hyperfields.Fields.Hypertopology.chainTopology, List.cons, List.nil
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
8 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 212
  before
```
⊢ chainTopology.closure [0, 1] = [0, 1, 2]
```
  after
  no goals remain
```
theorem chain_closure_of_open :
    chainTopology.closure [0, 1] = [0, 1, 2] := by
…
```
theorem Hyperfields.Fields.Hypertopology.chain_closure_of_closed The closure of the closed set {2} line 217 source
The closure of {2} in the chain topology is {2}.

A closed set's closure is itself, because it is one of its own closed supersets and the intersection cannot grow past it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, List, Fin, OfNat.ofNat, Nat, Hyperfields.Fields.Hypertopology.FiniteTopology.closure, Hyperfields.Fields.Hypertopology.chainTopology, List.cons, List.nil
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
8 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 219
  before
```
⊢ chainTopology.closure [2] = [2]
```
  after
  no goals remain
```
theorem chain_closure_of_closed :
    chainTopology.closure [2] = [2] := by
…
```
theorem Hyperfields.Fields.Hypertopology.chain_interior_of_carrier The interior of the whole carrier line 224 source
The interior of the whole carrier in the chain topology is the whole carrier.

The interior of the whole carrier is the whole carrier, because the carrier is open.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, List, Fin, OfNat.ofNat, Nat, Hyperfields.Fields.Hypertopology.FiniteTopology.interior, Hyperfields.Fields.Hypertopology.chainTopology, List.cons, List.nil
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
8 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 226
  before
```
⊢ chainTopology.interior [0, 1, 2] = [0, 1, 2]
```
  after
  no goals remain
```
theorem chain_interior_of_carrier :
    chainTopology.interior [0, 1, 2] = [0, 1, 2] := by
…
```
theorem Hyperfields.Fields.Hypertopology.chain_interior_of_tail The interior of the set {1, 2} line 231 source
The interior of {1, 2} in the chain topology is empty.

The interior is the largest open set inside the subset, and on the chain no nonempty open set lies inside `{1, 2}`.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, List, Fin, OfNat.ofNat, Nat, Hyperfields.Fields.Hypertopology.FiniteTopology.interior, Hyperfields.Fields.Hypertopology.chainTopology, List.cons, List.nil
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
7 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 233
  before
```
⊢ chainTopology.interior [1, 2] = []
```
  after
  no goals remain
```
theorem chain_interior_of_tail :
    chainTopology.interior [1, 2] = [] := by
…
```
theorem Hyperfields.Fields.Hypertopology.chain_interior_of_open The interior of the set {0, 1} line 238 source
The interior of {0, 1} in the chain topology is {0, 1}.

`{0, 1}` is itself open on the chain, so it is the largest open set inside itself and the interior is the set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, List, Fin, OfNat.ofNat, Nat, Hyperfields.Fields.Hypertopology.FiniteTopology.interior, Hyperfields.Fields.Hypertopology.chainTopology, List.cons, List.nil
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
8 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 240
  before
```
⊢ chainTopology.interior [0, 1] = [0, 1]
```
  after
  no goals remain
```
theorem chain_interior_of_open :
    chainTopology.interior [0, 1] = [0, 1] := by
…
```
theorem Hyperfields.Fields.Hypertopology.chain_boundary_of_open The boundary of the open set {0, 1} line 253 source
The boundary of {0, 1} in the chain topology is {2}.
The boundary is where the set and its complement meet. {0, 1} does not contain 2 and its complement {2} does not contain any of {0, 1}, so 2 is not a boundary point of the set itself; the boundary of the set is the closure of {0, 1} intersected with the closure of {2}, which is {2}.

A set that is open but not closed has a nonempty boundary, and on the chain the boundary of `{0, 1}` is the point that cannot be avoided.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, List, Fin, OfNat.ofNat, Nat, Hyperfields.Fields.Hypertopology.FiniteTopology.boundary, Hyperfields.Fields.Hypertopology.chainTopology, List.cons, List.nil
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
8 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 255
  before
```
⊢ chainTopology.boundary [0, 1] = [2]
```
  after
  no goals remain
```
theorem chain_boundary_of_open :
    chainTopology.boundary [0, 1] = [2] := by
…
```
theorem Hyperfields.Fields.Hypertopology.chain_boundary_of_singleton The boundary of the singleton {0} line 260 source
The boundary of {0} in the chain topology is {1, 2}.

An open singleton on a chain still has a boundary, because the chain continues past it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, List, Fin, OfNat.ofNat, Nat, Hyperfields.Fields.Hypertopology.FiniteTopology.boundary, Hyperfields.Fields.Hypertopology.chainTopology, List.cons, List.nil
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
8 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 262
  before
```
⊢ chainTopology.boundary [0] = [1, 2]
```
  after
  no goals remain
```
theorem chain_boundary_of_singleton :
    chainTopology.boundary [0] = [1, 2] := by
…
```
theorem Hyperfields.Fields.Hypertopology.chain_boundary_of_carrier The boundary of the whole carrier line 267 source
The boundary of the whole carrier in the chain topology is empty.

The carrier is closed, so its boundary is empty and the chain is connected.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, List, Fin, OfNat.ofNat, Nat, Hyperfields.Fields.Hypertopology.FiniteTopology.boundary, Hyperfields.Fields.Hypertopology.chainTopology, List.cons, List.nil
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
7 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 269
  before
```
⊢ chainTopology.boundary [0, 1, 2] = []
```
  after
  no goals remain
```
theorem chain_boundary_of_carrier :
    chainTopology.boundary [0, 1, 2] = [] := by
…
```
theorem Hyperfields.Fields.Hypertopology.chain_identity_is_continuous An identity map on the chain is continuous line 274 source
The identity map from the chain topology to itself is continuous.

The identity map pulls every open set back to itself, and every open set is open, so it is continuous.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hypertopology.continuousBetween, OfNat.ofNat, Nat, Hyperfields.Fields.Hypertopology.chainTopology, List.cons, Prod, Fin, Prod.mk, List.nil, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
7 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 276
  before
```
⊢ continuousBetween chainTopology chainTopology [(0, 0), (1, 1), (2, 2)] = true
```
  after
  no goals remain
```
theorem chain_identity_is_continuous :
    continuousBetween chainTopology chainTopology [(0, 0), (1, 1), (2, 2)] = true := by
…
```
Mentions: Hyperfields.Fields.Hypertopology.continuousBetween, Hyperfields.Fields.Hypertopology.chainTopology
theorem Hyperfields.Fields.Hypertopology.chain_to_discrete_is_continuous A map to a finer topology is continuous line 281 source
A constant map from the chain topology to the discrete two-point topology is continuous.

A constant map is continuous into any topology, because the preimage of every open set is either everything or nothing, and both are open.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hypertopology.continuousBetween, OfNat.ofNat, Nat, Hyperfields.Fields.Hypertopology.chainTopology, Hyperfields.Fields.Hypertopology.discreteTwo, List.cons, Prod, Fin, Prod.mk, List.nil, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
7 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 283
  before
```
⊢ continuousBetween chainTopology discreteTwo [(0, 0), (1, 0), (2, 0)] = true
```
  after
  no goals remain
```
theorem chain_to_discrete_is_continuous :
    continuousBetween chainTopology discreteTwo [(0, 0), (1, 0), (2, 0)] = true := by
…
```
Mentions: Hyperfields.Fields.Hypertopology.continuousBetween, Hyperfields.Fields.Hypertopology.chainTopology, Hyperfields.Fields.Hypertopology.discreteTwo
theorem Hyperfields.Fields.Hypertopology.chain_to_indiscrete_is_continuous A map to a coarser topology is continuous line 288 source
A map from the chain topology to the indiscrete two-point topology is continuous.

A coarser target has fewer obligations, so a total map that meets them is continuous.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hypertopology.continuousBetween, OfNat.ofNat, Nat, Hyperfields.Fields.Hypertopology.chainTopology, Hyperfields.Fields.Hypertopology.indiscreteTwo, List.cons, Prod, Fin, Prod.mk, List.nil, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
7 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 290
  before
```
⊢ continuousBetween chainTopology indiscreteTwo [(0, 0), (1, 0), (2, 0)] = true
```
  after
  no goals remain
```
theorem chain_to_indiscrete_is_continuous :
    continuousBetween chainTopology indiscreteTwo [(0, 0), (1, 0), (2, 0)] = true := by
…
```
Mentions: Hyperfields.Fields.Hypertopology.continuousBetween, Hyperfields.Fields.Hypertopology.chainTopology, Hyperfields.Fields.Hypertopology.indiscreteTwo
theorem Hyperfields.Fields.Hypertopology.a_noncontinuous_map_is_rejected A discontinuous map is rejected line 304 source
A map that pulls an open set back to a non-open set is not continuous.
This is the negative case. A checker that never rejects anything is not a check, and this theorem is what makes the positive cases meaningful.
The map sends 1 and 2 to different points of the discrete target, so the preimage of the target's open set {0} is {0}, which is not open in the chain topology. The map is therefore not continuous.

The continuity check must be able to fail, or it certifies nothing.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hypertopology.continuousBetween, OfNat.ofNat, Nat, Hyperfields.Fields.Hypertopology.chainTopology, Hyperfields.Fields.Hypertopology.discreteTwo, List.cons, Prod, Fin, Prod.mk, List.nil, Bool.false
Proof uses: of_decide_eq_true, id, Decidable.decide, Bool.true, Eq.refl
7 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 306
  before
```
⊢ continuousBetween chainTopology discreteTwo [(0, 0), (1, 1), (2, 0)] = false
```
  after
  no goals remain
```
theorem a_noncontinuous_map_is_rejected :
    continuousBetween chainTopology discreteTwo [(0, 0), (1, 1), (2, 0)] = false := by
…
```
Mentions: Hyperfields.Fields.Hypertopology.continuousBetween, Hyperfields.Fields.Hypertopology.chainTopology, Hyperfields.Fields.Hypertopology.discreteTwo
def Hyperfields.Fields.Hypertopology.entry Hypertopology explainer entry line 316 source
The canonical Hypertopology record used by the unified portal.

This declaration exposes the checked ecosystem record for Hypertopology on its own stable explainer page.
See also: Hyperfields.hypertopology

no axioms what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.hypertopology
```
def entry : Hyperfields.Entry := Hyperfields.hypertopology
…
```
Mentions: Hyperfields.Entry, Hyperfields.hypertopology