Neighborhood systems (Scott 1981, PRG-19, §1) — foundations

Following Dana Scott, Lectures on a Mathematical Theory of Computation, Technical Monograph PRG-19, Oxford (May 1981), Lecture I, Domains given by neighbourhoods.

Scott fixes a non-empty set Δ of tokens and considers a family 𝒟 of subsets of Δ (the neighbourhoods). The order is reversed relative to information: a smaller neighbourhood carries more information. A finite sequence of neighbourhoods is consistent when it has a common lower bound inside 𝒟 (a Z ∈ 𝒟 contained in all of them); a neighbourhood system is closed under intersections of consistent finite sequences.

This file formalizes the very first page of §1:

• Definition 1.1 — NeighborhoodSystem: a family with Δ ∈ 𝒟 (condition (i)) and closure under consistent binary intersections (condition (ii)).
• Factoid 1.1a / 1.1b — Scott's recursive convention for the finite intersection ⋂_{i < n} Xᵢ (interUpTo): the empty intersection is Δ, and the (n+1)-fold intersection peels off the last factor.
• Theorem 1.1c — "from (ii) we can extend the intersection property to any finite sequence", and consequently a finite sequence is consistent iff its intersection lies in 𝒟.

The §1 core is deliberately constructive: Scott uses partial filters so that the basic theory avoids maximal-filter existence (Zorn/choice). Every theorem here depends only on propext/Quot.sound (no Classical.choice).

structure Domain.Neighborhood.NeighborhoodSystem (α : Type u_1) : Type u_1

Definition 1.1 (Scott 1981, PRG-19). A neighbourhood system over a token type α. mem X means "X is a neighbourhood" (X ∈ 𝒟), and master is Scott's least informative neighbourhood Δ (the whole token set, "ask me no questions").

The two conditions are exactly Scott's:

• (i) Δ ∈ 𝒟 — master_mem;
• (ii) whenever X, Y, Z ∈ 𝒟 and Z ⊆ X ∩ Y, then X ∩ Y ∈ 𝒟 — inter_mem.

We keep master as a field (rather than hard-wiring Set.univ) to stay faithful to Scott's Δ notation, and record Scott's standing assumption 𝒟 ⊆ 𝒫(Δ) as the field sub_master (every neighbourhood is a subset of Δ). The latter is what makes the principal filter ↑X (Definition 1.7) contain Δ, and underlies the least element ⊥ = ↑Δ.

• mem : Set α → Prop

  mem X holds iff X is a neighbourhood of the system (X ∈ 𝒟).

• master : Set α

  Scott's distinguished least-informative neighbourhood Δ.

• master_mem : self.mem self.master

  (i) Δ ∈ 𝒟.

• inter_mem {X Y Z : Set α} : self.mem X → self.mem Y → self.mem Z → Z ⊆ X ∩ Y → self.mem (X ∩ Y)

  (ii) Closure under intersection of a consistent pair: if X, Y, Z ∈ 𝒟 with the witness Z ⊆ X ∩ Y, then X ∩ Y ∈ 𝒟.

• sub_master {X : Set α} : self.mem X → X ⊆ self.master

  Scott's 𝒟 ⊆ 𝒫(Δ): every neighbourhood is a subset of the master neighbourhood Δ.

def Domain.Neighborhood.NestedOrDisjoint {α : Type u_1} (mem : Set α → Prop) : Prop

Scott's "very special circumstance" (the prose after Examples 1.2–1.4): a family 𝒟 is nested-or-disjoint when any two of its members are either nested (one included in the other) or disjoint.

Equations

• Domain.Neighborhood.NestedOrDisjoint mem = ∀ ⦃X Y : Set α⦄, mem X → mem Y → X ⊆ Y ∨ Y ⊆ X ∨ X ∩ Y = ∅

def Domain.Neighborhood.NeighborhoodSystem.ofNestedOrDisjoint {α : Type u_1} (mem : Set α → Prop) (master : Set α) (master_mem : mem master) (hnd : NestedOrDisjoint mem) (sub_master : ∀ {X : Set α}, mem X → X ⊆ master) : NeighborhoodSystem α

Factoid 1.4a (Scott 1981, PRG-19). "In these systems two neighbourhoods are either disjoint or one is included in the other": a family containing Δ whose members are pairwise nested-or-disjoint is a neighbourhood system. This uniformly explains why Examples 1.2, 1.3 and 1.4 satisfy Definition 1.1.

The verification of condition (ii) needs no choice: if X, Y are nested then X ∩ Y is the smaller (already in 𝒟); if they are disjoint then the consistency witness Z ⊆ X ∩ Y = ∅ forces Z = ∅, whence X ∩ Y = ∅ = Z ∈ 𝒟. The caller supplies sub_master (Scott's 𝒟 ⊆ 𝒫(Δ)) directly.

Equations

• Domain.Neighborhood.NeighborhoodSystem.ofNestedOrDisjoint mem master master_mem hnd sub_master = { mem := mem, master := master, master_mem := master_mem, inter_mem := ⋯, sub_master := ⋯ }

def Domain.Neighborhood.NeighborhoodSystem.IsPositive {α : Type u_1} (V : NeighborhoodSystem α) : Prop

Exercise 1.19 (Scott 1981, PRG-19) — positivity, condition (ii′). A neighbourhood system is positive when Scott's (ii) is strengthened to the biconditional (ii′): for X, Y ∈ 𝒟, the intersection X ∩ Y is a neighbourhood iff it is non-empty.

Equations

• V.IsPositive = ∀ ⦃X Y : Set α⦄, V.mem X → V.mem Y → (V.mem (X ∩ Y) ↔ (X ∩ Y).Nonempty)

def Domain.Neighborhood.NeighborhoodSystem.ofPositive {α : Type u_1} (mem : Set α → Prop) (master : Set α) (master_mem : mem master) (sub_master : ∀ {X : Set α}, mem X → X ⊆ master) (pos : ∀ ⦃X Y : Set α⦄, mem X → mem Y → (mem (X ∩ Y) ↔ (X ∩ Y).Nonempty)) : NeighborhoodSystem α

Exercise 1.19 — a positive system is a neighbourhood system. Scott: "prove that a positive neighbourhood system is indeed a neighbourhood system". From the raw data — (i) Δ ∈ 𝒟, 𝒟 ⊆ 𝒫(Δ), and the positivity axiom (ii′) — condition (ii) follows: a consistency witness Z ⊆ X ∩ Y with Z ∈ 𝒟 is itself non-empty (apply (ii′) to Z ∩ Z = Z), so X ∩ Y ⊇ Z is non-empty, whence X ∩ Y ∈ 𝒟 by (ii′). Choice-free.

Equations

• Domain.Neighborhood.NeighborhoodSystem.ofPositive mem master master_mem sub_master pos = { mem := mem, master := master, master_mem := master_mem, inter_mem := ⋯, sub_master := ⋯ }

theorem Domain.Neighborhood.NeighborhoodSystem.ofPositive_isPositive {α : Type u_1} (mem : Set α → Prop) (master : Set α) (master_mem : mem master) (sub_master : ∀ {X : Set α}, mem X → X ⊆ master) (pos : ∀ ⦃X Y : Set α⦄, mem X → mem Y → (mem (X ∩ Y) ↔ (X ∩ Y).Nonempty)) : (ofPositive mem master master_mem ⋯ pos).IsPositive

The system built by ofPositive is indeed positive.

def Domain.Neighborhood.NeighborhoodSystem.interUpTo {α : Type u_1} (V : NeighborhoodSystem α) (X : ℕ → Set α) : ℕ → Set α

The finite intersection ⋂_{i < n} Xᵢ of the first n terms of a sequence of neighbourhoods, defined by Scott's recursive convention (Factoid 1.1a / 1.1b):

• n = 0 : the empty intersection is Δ (master);
• n + 1 : (⋂_{i < n} Xᵢ) ∩ Xₙ.

(See interUpTo_zero and interUpTo_succ for the two defining equations as lemmas.)

Equations

• V.interUpTo X 0 = V.master
• V.interUpTo X n.succ = V.interUpTo X n ∩ X n

@[simp]

theorem Domain.Neighborhood.NeighborhoodSystem.interUpTo_zero {α : Type u_1} (V : NeighborhoodSystem α) (X : ℕ → Set α) : V.interUpTo X 0 = V.master

Factoid 1.1a. The intersection of the empty sequence of neighbourhoods is Δ: ⋂_{i < 0} Xᵢ = Δ.

@[simp]

theorem Domain.Neighborhood.NeighborhoodSystem.interUpTo_succ {α : Type u_1} (V : NeighborhoodSystem α) (X : ℕ → Set α) (n : ℕ) : V.interUpTo X (n + 1) = V.interUpTo X n ∩ X n

Factoid 1.1b. The intersection of the first n + 1 neighbourhoods peels off the last factor: ⋂_{i < n+1} Xᵢ = (⋂_{i < n} Xᵢ) ∩ Xₙ.

theorem Domain.Neighborhood.NeighborhoodSystem.interUpTo_subset {α : Type u_1} (V : NeighborhoodSystem α) (X : ℕ → Set α) {n j : ℕ} : j < n → V.interUpTo X n ⊆ X j

The finite intersection is contained in each of its factors: ⋂_{i < n} Xᵢ ⊆ Xⱼ for j < n. (Supporting lemma: this is what makes ⋂_{i < n} Xᵢ a common lower bound of the sequence, the intuition behind consistency.)

def Domain.Neighborhood.NeighborhoodSystem.Consistent {α : Type u_1} (V : NeighborhoodSystem α) (X : ℕ → Set α) (n : ℕ) : Prop

A finite sequence X₀, …, Xₙ₋₁ of neighbourhoods is consistent in 𝒟 when it has a common lower bound inside 𝒟: some Z ∈ 𝒟 contained in the intersection ⋂_{i < n} Xᵢ (equivalently, contained in every Xⱼ, j < n). This is Scott's notion of consistency, generalized from pairs to finite sequences.

Equations

• V.Consistent X n = ∃ (Z : Set α), V.mem Z ∧ Z ⊆ V.interUpTo X n

theorem Domain.Neighborhood.NeighborhoodSystem.interUpTo_mem {α : Type u_1} (V : NeighborhoodSystem α) (X : ℕ → Set α) {n : ℕ} : (∀ (i : ℕ), i < n → V.mem (X i)) → V.Consistent X n → V.mem (V.interUpTo X n)

Theorem 1.1c (extension of the intersection property). Scott: "from (ii), we can extend the intersection property to any finite sequence." If Xᵢ ∈ 𝒟 for every i < n and the sequence is consistent, then the finite intersection ⋂_{i < n} Xᵢ is again a neighbourhood (∈ 𝒟). Proved by induction on n; the inductive step is one application of condition (ii).

theorem Domain.Neighborhood.NeighborhoodSystem.consistent_iff_interUpTo_mem {α : Type u_1} (V : NeighborhoodSystem α) (X : ℕ → Set α) {n : ℕ} (hX : ∀ (i : ℕ), i < n → V.mem (X i)) : V.Consistent X n ↔ V.mem (V.interUpTo X n)

Theorem 1.1c (consistency characterization). "Consequently, X₀, …, Xₙ₋₁ is consistent in 𝒟 iff ⋂_{i < n} Xᵢ ∈ 𝒟." (Given Xᵢ ∈ 𝒟 for all i < n.)

• → is the extension property interUpTo_mem;
• ← is immediate: the intersection is its own common lower bound.

structure Domain.Neighborhood.NeighborhoodSystem.Element {α : Type u_1} (V : NeighborhoodSystem α) : Type u_1

Definition 1.6 (Scott 1981, PRG-19). An (ideal) element of a neighbourhood system: a subfamily x ⊆ 𝒟 that is a filter — (i) Δ ∈ x, (ii) closed under intersection, (iii) upward closed within 𝒟. The domain is the type Element of all such filters, ordered by inclusion.

• mem : Set α → Prop

  mem X holds iff the neighbourhood X belongs to the filter x.

• sub {X : Set α} : self.mem X → V.mem X

  x is a subfamily of 𝒟.

• master_mem : self.mem V.master

  (i) Δ ∈ x.

• inter_mem {X Y : Set α} : self.mem X → self.mem Y → self.mem (X ∩ Y)

  (ii) X, Y ∈ x ⟹ X ∩ Y ∈ x.

• up_mem {X Y : Set α} : self.mem X → V.mem Y → X ⊆ Y → self.mem Y

  (iii) X ∈ x and X ⊆ Y ∈ 𝒟 ⟹ Y ∈ x.

theorem Domain.Neighborhood.NeighborhoodSystem.Element.ext {α : Type u_1} (V : NeighborhoodSystem α) {x y : V.Element} (h : ∀ (X : Set α), x.mem X ↔ y.mem X) : x = y

Two elements with the same membership predicate are equal (the remaining fields are Props).

theorem Domain.Neighborhood.NeighborhoodSystem.Element.mem_interUpTo {α : Type u_2} {V : NeighborhoodSystem α} (x : V.Element) (X : ℕ → Set α) {n : ℕ} : (∀ (i : ℕ), i < n → x.mem (X i)) → x.mem (V.interUpTo X n)

A filter (Element) is closed under the finite intersection ⋂_{i<n} Xᵢ: if every factor Xᵢ (i < n) lies in the filter x, so does interUpTo X n. Used in Exercises 1.18 and 1.21. Base case x.master_mem; inductive step one x.inter_mem.

theorem Domain.Neighborhood.NeighborhoodSystem.Element.mem_interUpTo_iff {α : Type u_2} {V : NeighborhoodSystem α} (x : V.Element) (X : ℕ → Set α) {n : ℕ} (hX : ∀ (i : ℕ), i < n → V.mem (X i)) : x.mem (V.interUpTo X n) ↔ ∀ (i : ℕ), i < n → x.mem (X i)

Membership of the finite intersection in a filter, as a biconditional (given all factors are neighbourhoods). → is upward closure along interUpTo X n ⊆ Xᵢ (interUpTo_subset); ← is Element.mem_interUpTo.

@[implicit_reducible]

instance Domain.Neighborhood.NeighborhoodSystem.instPartialOrderElement {α : Type u_1} (V : NeighborhoodSystem α) : PartialOrder V.Element

Elements are ordered by inclusion of their membership predicates (Scott's approximation order, Definition 1.8).

Equations

• V.instPartialOrderElement = { le := fun (x y : V.Element) => ∀ (X : Set α), x.mem X → y.mem X, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

def Domain.Neighborhood.NeighborhoodSystem.limitFamily {α : Type u_1} (V : NeighborhoodSystem α) (X : ℕ → Set α) : Set (Set α)

The limit family of a sequence of neighbourhoods (Scott, the prose before Definition 1.6): x = {Z ∈ 𝒟 ∣ Xₙ ⊆ Z for some n} — the family of all neighbourhoods eventually reached by ⟨Xₙ⟩. This is the construction Scott uses to motivate the (ideal) elements of |𝒟|.

Equations

• V.limitFamily X = {Z : Set α | V.mem Z ∧ ∃ (n : ℕ), X n ⊆ Z}

def Domain.Neighborhood.NeighborhoodSystem.SeqEquiv {α : Type u_1} (X Y : ℕ → Set α) : Prop

Two sequences of neighbourhoods are equivalent ("each goes equally deep as the other"): for every Yₘ some Xₙ ⊆ Yₘ, and for every Xₙ some Yₘ ⊆ Xₙ.

Equations

• Domain.Neighborhood.NeighborhoodSystem.SeqEquiv X Y = ((∀ (m : ℕ), ∃ (n : ℕ), X n ⊆ Y m) ∧ ∀ (n : ℕ), ∃ (m : ℕ), Y m ⊆ X n)

theorem Domain.Neighborhood.NeighborhoodSystem.limitFamily_eq_iff {α : Type u_1} (V : NeighborhoodSystem α) (X Y : ℕ → Set α) (hX : ∀ (n : ℕ), V.mem (X n)) (hY : ∀ (m : ℕ), V.mem (Y m)) : V.limitFamily X = V.limitFamily Y ↔ SeqEquiv X Y

Factoid 1.5b (Scott 1981, PRG-19). "It is easy to prove that … the two families are equal if and only if the sequences are equivalent." Given that every term of each sequence is a neighbourhood, the limit families coincide exactly when the sequences are equivalent.

def Domain.Neighborhood.NeighborhoodSystem.principal {α : Type u_1} (V : NeighborhoodSystem α) {X : Set α} (hX : V.mem X) : V.Element

Definition 1.7 (Scott 1981, PRG-19). The principal filter ↑X determined by a neighbourhood X ∈ 𝒟:

↑X = {Y ∈ 𝒟 ∣ X ⊆ Y}.

These are Scott's finite elements of |𝒟|. The four filter conditions:

• sub is the first projection (Y ∈ ↑X ⟹ Y ∈ 𝒟);
• master_mem needs X ⊆ Δ, supplied by V.sub_master (Scott's 𝒟 ⊆ 𝒫(Δ));
• inter_mem uses Set.subset_inter (from X ⊆ Y₁, X ⊆ Y₂) with X itself as the consistency witness for V.inter_mem;
• up_mem is transitivity of ⊆.

Equations

• V.principal hX = { mem := fun (Y : Set α) => V.mem Y ∧ X ⊆ Y, sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

@[simp]

theorem Domain.Neighborhood.NeighborhoodSystem.mem_principal {α : Type u_1} (V : NeighborhoodSystem α) {X Y : Set α} (hX : V.mem X) : (V.principal hX).mem Y ↔ V.mem Y ∧ X ⊆ Y

theorem Domain.Neighborhood.NeighborhoodSystem.principal_le_iff {α : Type u_1} (V : NeighborhoodSystem α) {X Y : Set α} (hX : V.mem X) (hY : V.mem Y) : V.principal hX ≤ V.principal hY ↔ Y ⊆ X

Factoid 1.7a (Scott 1981, PRG-19) — inclusion-reversing. "It is obvious that the correspondence between X and ↑X is one-one and inclusion reversing." The order on ↑: ↑X ⊑ ↑Y ↔ Y ⊆ X (equivalently Scott's X ⊆ Y ↔ ↑Y ⊑ ↑X).

→ tests at Z = X (X ∈ ↑X since X ⊆ X), reading off Y ⊆ X from X ∈ ↑Y; ← chains Y ⊆ X ⊆ Z.

theorem Domain.Neighborhood.NeighborhoodSystem.principal_injective {α : Type u_1} (V : NeighborhoodSystem α) {X Y : Set α} (hX : V.mem X) (hY : V.mem Y) (h : V.principal hX = V.principal hY) : X = Y

Factoid 1.7a (Scott 1981, PRG-19) — one-one. The correspondence X ↦ ↑X is injective: ↑X = ↑Y ⟹ X = Y. Antisymmetry applied to principal_le_iff in both directions.

theorem Domain.Neighborhood.NeighborhoodSystem.eq_iUnion_principal {α : Type u_1} (V : NeighborhoodSystem α) (x : V.Element) {Z : Set α} : x.mem Z ↔ ∃ (X : Set α), ∃ (hX : x.mem X), (V.principal ⋯).mem Z

Factoid 1.7b (Scott 1981, PRG-19). "It is also obvious from the definitions that for each x ∈ |𝒟|, x = ⋃ {↑X ∣ X ∈ x}." In membership form (the union over a Set (Set α) made concrete): a neighbourhood Z is in x iff Z lies in the principal filter ↑X of some member X of x.

→ uses X = Z (Z ∈ ↑Z as Z ⊆ Z); ← is upward closure up_mem (X ⊆ Z, Z ∈ 𝒟).

def Domain.Neighborhood.NeighborhoodSystem.bot {α : Type u_1} (V : NeighborhoodSystem α) : V.Element

Definition 1.8 (Scott 1981, PRG-19) — ⊥. The least defined element ⊥ = {Δ}, "read: bottom". It is the principal filter of the master neighbourhood Δ: ⊥ = ↑Δ.

Equations

• V.bot = V.principal ⋯

@[simp]

theorem Domain.Neighborhood.NeighborhoodSystem.mem_bot {α : Type u_1} (V : NeighborhoodSystem α) {Y : Set α} : V.bot.mem Y ↔ Y = V.master

Definition 1.8 — ⊥ = {Δ} literally. Scott's ⊥ is the singleton {Δ}: a neighbourhood Y belongs to ⊥ iff Y = Δ.

→: Y ∈ ⊥ = ↑Δ gives Y ∈ 𝒟 and Δ ⊆ Y; V.sub_master gives the reverse Y ⊆ Δ, so Y = Δ by antisymmetry. ←: Δ ∈ 𝒟 and Δ ⊆ Δ.

theorem Domain.Neighborhood.NeighborhoodSystem.bot_le {α : Type u_1} (V : NeighborhoodSystem α) (x : V.Element) : V.bot ≤ x

Factoid 1.8a (Scott 1981, PRG-19). "The element that approximates all others, {Δ}, is called ⊥": ⊥ is the least element of |𝒟|, ⊥ ⊑ x for every x.

Given Y ∈ ⊥, i.e. Y = Δ, membership Δ ∈ x is filter condition (i) (x.master_mem).

@[implicit_reducible]

instance Domain.Neighborhood.NeighborhoodSystem.instOrderBotElement {α : Type u_1} (V : NeighborhoodSystem α) : OrderBot V.Element

Factoid 1.8a, packaged. ⊥ is an OrderBot for the approximation order, so the ⊥ notation refers to {Δ}. Constructive (bot_le is [propext, Quot.sound]).

Equations

• V.instOrderBotElement = { bot := V.bot, bot_le := ⋯ }

def Domain.Neighborhood.NeighborhoodSystem.IsTotal {α : Type u_1} (V : NeighborhoodSystem α) (x : V.Element) : Prop

Definition 1.8 (Scott 1981, PRG-19) — total elements. "Elements maximal with respect to the approximation relation are called total elements." x is total iff it is maximal: any y it approximates approximates it back. This is the predicate only; the existence of total elements above a given x (Exercise 1.24) is choice-dependent and out of scope here.

Equations

• V.IsTotal x = ∀ (y : V.Element), x ≤ y → y ≤ x

theorem Domain.Neighborhood.NeighborhoodSystem.eq_principal_of_isMin {α : Type u_1} (V : NeighborhoodSystem α) (x : V.Element) {X : Set α} (hX : x.mem X) (hmin : ∀ (Y : Set α), x.mem Y → X ⊆ Y) : x = V.principal ⋯

Factoid 1.8b (Scott 1981, PRG-19) — "Examples 1.2–1.5 revisited". "Any explicitly given filter x is principal … the minimal X ∈ x tells us all we need to know." Stated honestly: if the filter x has a ⊆-minimum member X (one contained in every member of x), then x is exactly the principal filter ↑X. In a finite system every filter has such a minimum (the intersection of its finitely many members, itself in x by closure), so every element is principal; that finiteness step is the only classical ingredient and is left implicit here — this constructive core captures the content.

⊆: any Z ∈ x satisfies X ⊆ Z by minimality, so Z ∈ ↑X. ⊇: Z ∈ ↑X means Z ∈ 𝒟 and X ⊆ Z, so Z ∈ x by upward closure from X ∈ x.

@[reducible, inline]

abbrev Domain.Neighborhood.DomainIso {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : Type (max u_2 u_1)

Definition 1.9 (Scott 1981, PRG-19). Two neighbourhood systems 𝒟₀ and 𝒟₁ (over possibly different token types) determine isomorphic domains iff there is a one-one, inclusion-preserving correspondence between |𝒟₀| and |𝒟₁|. We package "one-one + preserves inclusion (both ways)" as mathlib's order-isomorphism ≃o: an OrderIso is automatically a bijection that reflects as well as preserves ⊑ (map_rel_iff), which is exactly Scott's requirement.

Equations

• Domain.Neighborhood.DomainIso V₀ V₁ = (V₀.Element ≃o V₁.Element)

def Domain.Neighborhood.Isomorphic {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : Prop

Scott's 𝒟₀ ≅ 𝒟₁: the domains are isomorphic (there exists a DomainIso).

Equations

• (V₀ ≅ᴰ V₁) = Nonempty (Domain.Neighborhood.DomainIso V₀ V₁)

def Domain.Neighborhood.«term_≅ᴰ_» : Lean.TrailingParserDescr

Scott's 𝒟₀ ≅ 𝒟₁: the domains are isomorphic (there exists a DomainIso).

Equations

• One or more equations did not get rendered due to their size.

theorem Domain.Neighborhood.Isomorphic.refl {α : Type u_1} (V : NeighborhoodSystem α) : V ≅ᴰ V

≅ᴰ is reflexive (OrderIso.refl).

theorem Domain.Neighborhood.Isomorphic.symm {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (h : V₀ ≅ᴰ V₁) : V₁ ≅ᴰ V₀

≅ᴰ is symmetric (OrderIso.symm).

theorem Domain.Neighborhood.Isomorphic.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (h₀ : V₀ ≅ᴰ V₁) (h₁ : V₁ ≅ᴰ V₂) : V₀ ≅ᴰ V₂

≅ᴰ is transitive (OrderIso.trans).