Home Metamath Proof ExplorerTheorem List (p. 383 of 424) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

 Color key: Metamath Proof Explorer (1-27745) Hilbert Space Explorer (27746-29270) Users' Mathboxes (29271-42316)

Theorem List for Metamath Proof Explorer - 38201-38300   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremntrneineine0lem 38201* If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then conditions equal to claiming that for every point, at least one (pseudo-)neighborbood exists hold equally. (Contributed by RP, 29-May-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)    &   (𝜑𝑋𝐵)       (𝜑 → (∃𝑠 ∈ 𝒫 𝐵𝑋 ∈ (𝐼𝑠) ↔ (𝑁𝑋) ≠ ∅))

Theoremntrneineine1lem 38202* If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then conditions equal to claiming that for every point, at not all subsets are (pseudo-)neighborboods hold equally. (Contributed by RP, 1-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)    &   (𝜑𝑋𝐵)       (𝜑 → (∃𝑠 ∈ 𝒫 𝐵 ¬ 𝑋 ∈ (𝐼𝑠) ↔ (𝑁𝑋) ≠ 𝒫 𝐵))

Theoremntrneifv4 38203* The value of the interior (closure) expressed in terms of the neighbors (convergents) function. (Contributed by RP, 26-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)    &   (𝜑𝑆 ∈ 𝒫 𝐵)       (𝜑 → (𝐼𝑆) = {𝑥𝐵𝑆 ∈ (𝑁𝑥)})

Theoremntrneiel2 38204* Membership in iterated interior of a set is equivalent to there existing a particular neighborhood of that member such that points are members of that neighborhood if and only if the set is a neighborhood of each of those points. (Contributed by RP, 11-Jul-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)    &   (𝜑𝑋𝐵)    &   (𝜑𝑆 ∈ 𝒫 𝐵)       (𝜑 → (𝑋 ∈ (𝐼‘(𝐼𝑆)) ↔ ∃𝑢 ∈ (𝑁𝑋)∀𝑦𝐵 (𝑦𝑢𝑆 ∈ (𝑁𝑦))))

Theoremntrneineine0 38205* If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then conditions equal to claiming that for every point, at least one (pseudo-)neighborbood exists hold equally. (Contributed by RP, 29-May-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)       (𝜑 → (∀𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑥 ∈ (𝐼𝑠) ↔ ∀𝑥𝐵 (𝑁𝑥) ≠ ∅))

Theoremntrneineine1 38206* If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then conditions equal to claiming that for every point, at not all subsets are (pseudo-)neighborboods hold equally. (Contributed by RP, 1-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)       (𝜑 → (∀𝑥𝐵𝑠 ∈ 𝒫 𝐵 ¬ 𝑥 ∈ (𝐼𝑠) ↔ ∀𝑥𝐵 (𝑁𝑥) ≠ 𝒫 𝐵))

Theoremntrneicls00 38207* If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then conditions equal to claiming that the closure of the empty set is the empty set hold equally. (Contributed by RP, 2-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)       (𝜑 → ((𝐼𝐵) = 𝐵 ↔ ∀𝑥𝐵 𝐵 ∈ (𝑁𝑥)))

Theoremntrneicls11 38208* If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then conditions equal to claiming that the interior of the empty set is the empty set hold equally. (Contributed by RP, 2-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)       (𝜑 → ((𝐼‘∅) = ∅ ↔ ∀𝑥𝐵 ¬ ∅ ∈ (𝑁𝑥)))

Theoremntrneiiso 38209* If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then conditions equal to claiming that the interior function is isotonic hold equally. (Contributed by RP, 3-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)       (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(𝑠𝑡 → (𝐼𝑠) ⊆ (𝐼𝑡)) ↔ ∀𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁𝑥) ∧ 𝑠𝑡) → 𝑡 ∈ (𝑁𝑥))))

Theoremntrneik2 38210* An interior function is contracting if and only if all the neighborhoods of a point contain that point. (Contributed by RP, 11-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)       (𝜑 → (∀𝑠 ∈ 𝒫 𝐵(𝐼𝑠) ⊆ 𝑠 ↔ ∀𝑥𝐵𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁𝑥) → 𝑥𝑠)))

Theoremntrneix2 38211* An interior (closure) function is expansive if and only if all subsets which contain a point are neighborhoods (convergents) of that point. (Contributed by RP, 11-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)       (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑠 ⊆ (𝐼𝑠) ↔ ∀𝑥𝐵𝑠 ∈ 𝒫 𝐵(𝑥𝑠𝑠 ∈ (𝑁𝑥))))

Theoremntrneikb 38212* The interiors of disjoint sets are disjoint if and only if the neighborhoods of every point contain no disjoint sets. (Contributed by RP, 11-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)       (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = ∅ → ((𝐼𝑠) ∩ (𝐼𝑡)) = ∅) ↔ ∀𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁𝑥) ∧ 𝑡 ∈ (𝑁𝑥)) → (𝑠𝑡) ≠ ∅)))

Theoremntrneixb 38213* The interiors (closures) of sets that span the base set also span the base set if and only if the neighborhoods (convergents) of every point contain at least one of every pair of sets that span the base set. (Contributed by RP, 11-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)       (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = 𝐵 → ((𝐼𝑠) ∪ (𝐼𝑡)) = 𝐵) ↔ ∀𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) = 𝐵 → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))

Theoremntrneik3 38214* The intersection of interiors of any pair is a subset of the interior of the intersection if and only if the intersection of any two neighborhoods of a point is also a neighborhood. (Contributed by RP, 19-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)       (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝐼𝑠) ∩ (𝐼𝑡)) ⊆ (𝐼‘(𝑠𝑡)) ↔ ∀𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁𝑥) ∧ 𝑡 ∈ (𝑁𝑥)) → (𝑠𝑡) ∈ (𝑁𝑥))))

Theoremntrneix3 38215* The closure of the union of any pair is a subset of the union of closures if and only if the union of any pair belonging to the convergents of a point implies at least one of the pair belongs to the the convergents of that point. (Contributed by RP, 19-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)       (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠𝑡)) ⊆ ((𝐼𝑠) ∪ (𝐼𝑡)) ↔ ∀𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) ∈ (𝑁𝑥) → (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))

Theoremntrneik13 38216* The interior of the intersection of any pair equals intersection of interiors if and only if the intersection of any pair belonging to the neighborhood of a point is equivalent to both of the pair belonging to the neighborhood of that point. (Contributed by RP, 19-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)       (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠𝑡)) = ((𝐼𝑠) ∩ (𝐼𝑡)) ↔ ∀𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) ∈ (𝑁𝑥) ↔ (𝑠 ∈ (𝑁𝑥) ∧ 𝑡 ∈ (𝑁𝑥)))))

Theoremntrneix13 38217* The closure of the union of any pair is equal to the union of closures if and only if the union of any pair belonging to the convergents of a point if equivalent to at least one of the pain belonging to the convergents of that point. (Contributed by RP, 19-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)       (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠𝑡)) = ((𝐼𝑠) ∪ (𝐼𝑡)) ↔ ∀𝑥𝐵𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵((𝑠𝑡) ∈ (𝑁𝑥) ↔ (𝑠 ∈ (𝑁𝑥) ∨ 𝑡 ∈ (𝑁𝑥)))))

Theoremntrneik4w 38218* Idempotence of the interior function is equivalent to saying a set is a neighborhood of a point if and only if the interior of the set is a neighborhood of a point. (Contributed by RP, 11-Jul-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)       (𝜑 → (∀𝑠 ∈ 𝒫 𝐵(𝐼‘(𝐼𝑠)) = (𝐼𝑠) ↔ ∀𝑥𝐵𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁𝑥) ↔ (𝐼𝑠) ∈ (𝑁𝑥))))

Theoremntrneik4 38219* Idempotence of the interior function is equivalent to stating a set, 𝑠, is a neighborhood of a point, 𝑥 is equivalent to there existing a special neighborhood, 𝑢, of 𝑥 such that a point is an element of the special neighborhood if and only if 𝑠 is also a neighborhood of the point. (Contributed by RP, 11-Jul-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   (𝜑𝐼𝐹𝑁)       (𝜑 → (∀𝑠 ∈ 𝒫 𝐵(𝐼‘(𝐼𝑠)) = (𝐼𝑠) ↔ ∀𝑥𝐵𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁𝑥) ↔ ∃𝑢 ∈ (𝑁𝑥)∀𝑦𝐵 (𝑦𝑢𝑠 ∈ (𝑁𝑦)))))

Theoremclsneibex 38220 If (pseudo-)closure and (pseudo-)neighborhood functions are related by the composite operator, 𝐻, then the base set exists. (Contributed by RP, 4-Jun-2021.)
𝐷 = (𝑃𝐵)    &   𝐻 = (𝐹𝐷)    &   (𝜑𝐾𝐻𝑁)       (𝜑𝐵 ∈ V)

Theoremclsneircomplex 38221 The relative complement of the class 𝑆 exists as a subset of the base set. (Contributed by RP, 26-Jun-2021.)
𝐷 = (𝑃𝐵)    &   𝐻 = (𝐹𝐷)    &   (𝜑𝐾𝐻𝑁)       (𝜑 → (𝐵𝑆) ∈ 𝒫 𝐵)

Theoremclsneif1o 38222* If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the 𝐻 operator, then the operator is a one-to-one, onto mapping. (Contributed by RP, 5-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛𝑚 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛𝑜))))))    &   𝐷 = (𝑃𝐵)    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   𝐻 = (𝐹𝐷)    &   (𝜑𝐾𝐻𝑁)       (𝜑𝐻:(𝒫 𝐵𝑚 𝒫 𝐵)–1-1-onto→(𝒫 𝒫 𝐵𝑚 𝐵))

Theoremclsneicnv 38223* If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the 𝐻 operator, then the converse of the operator is known. (Contributed by RP, 5-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛𝑚 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛𝑜))))))    &   𝐷 = (𝑃𝐵)    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   𝐻 = (𝐹𝐷)    &   (𝜑𝐾𝐻𝑁)       (𝜑𝐻 = (𝐷 ∘ (𝐵𝑂𝒫 𝐵)))

Theoremclsneikex 38224* If closure and neighborhoods functions are related, the closure function exists. (Contributed by RP, 27-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛𝑚 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛𝑜))))))    &   𝐷 = (𝑃𝐵)    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   𝐻 = (𝐹𝐷)    &   (𝜑𝐾𝐻𝑁)       (𝜑𝐾 ∈ (𝒫 𝐵𝑚 𝒫 𝐵))

Theoremclsneinex 38225* If closure and neighborhoods functions are related, the neighborhoods function exists. (Contributed by RP, 27-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛𝑚 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛𝑜))))))    &   𝐷 = (𝑃𝐵)    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   𝐻 = (𝐹𝐷)    &   (𝜑𝐾𝐻𝑁)       (𝜑𝑁 ∈ (𝒫 𝒫 𝐵𝑚 𝐵))

Theoremclsneiel1 38226* If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the 𝐻 operator, then membership in the closure of a subset is equivalent to the complement of the subset not being a neighborhood of the point. (Contributed by RP, 7-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛𝑚 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛𝑜))))))    &   𝐷 = (𝑃𝐵)    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   𝐻 = (𝐹𝐷)    &   (𝜑𝐾𝐻𝑁)    &   (𝜑𝑋𝐵)    &   (𝜑𝑆 ∈ 𝒫 𝐵)       (𝜑 → (𝑋 ∈ (𝐾𝑆) ↔ ¬ (𝐵𝑆) ∈ (𝑁𝑋)))

Theoremclsneiel2 38227* If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the 𝐻 operator, then membership in the closure of the complement of a subset is equivalent to the subset not being a neighborhood of the point. (Contributed by RP, 7-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛𝑚 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛𝑜))))))    &   𝐷 = (𝑃𝐵)    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   𝐻 = (𝐹𝐷)    &   (𝜑𝐾𝐻𝑁)    &   (𝜑𝑋𝐵)    &   (𝜑𝑆 ∈ 𝒫 𝐵)       (𝜑 → (𝑋 ∈ (𝐾‘(𝐵𝑆)) ↔ ¬ 𝑆 ∈ (𝑁𝑋)))

Theoremclsneifv3 38228* Value of the neighborhoods (convergents) in terms of the closure (interior) function. (Contributed by RP, 27-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛𝑚 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛𝑜))))))    &   𝐷 = (𝑃𝐵)    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   𝐻 = (𝐹𝐷)    &   (𝜑𝐾𝐻𝑁)    &   (𝜑𝑋𝐵)       (𝜑 → (𝑁𝑋) = {𝑠 ∈ 𝒫 𝐵 ∣ ¬ 𝑋 ∈ (𝐾‘(𝐵𝑠))})

Theoremclsneifv4 38229* Value of the the closure (interior) function in terms of the neighborhoods (convergents) function. (Contributed by RP, 27-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛𝑚 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛𝑜))))))    &   𝐷 = (𝑃𝐵)    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   𝐻 = (𝐹𝐷)    &   (𝜑𝐾𝐻𝑁)    &   (𝜑𝑆 ∈ 𝒫 𝐵)       (𝜑 → (𝐾𝑆) = {𝑥𝐵 ∣ ¬ (𝐵𝑆) ∈ (𝑁𝑥)})

Theoremneicvgbex 38230 If (pseudo-)neighborhood and (pseudo-)convergent functions are related by the composite operator, 𝐻, then the base set exists. (Contributed by RP, 4-Jun-2021.)
𝐷 = (𝑃𝐵)    &   𝐻 = (𝐹 ∘ (𝐷𝐺))    &   (𝜑𝑁𝐻𝑀)       (𝜑𝐵 ∈ V)

Theoremneicvgrcomplex 38231 The relative complement of the class 𝑆 exists as a subset of the base set. (Contributed by RP, 26-Jun-2021.)
𝐷 = (𝑃𝐵)    &   𝐻 = (𝐹 ∘ (𝐷𝐺))    &   (𝜑𝑁𝐻𝑀)       (𝜑 → (𝐵𝑆) ∈ 𝒫 𝐵)

Theoremneicvgf1o 38232* If neighborhood and convergent functions are related by operator 𝐻, it is a one-to-one onto relation. (Contributed by RP, 11-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛𝑚 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛𝑜))))))    &   𝐷 = (𝑃𝐵)    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   𝐺 = (𝐵𝑂𝒫 𝐵)    &   𝐻 = (𝐹 ∘ (𝐷𝐺))    &   (𝜑𝑁𝐻𝑀)       (𝜑𝐻:(𝒫 𝒫 𝐵𝑚 𝐵)–1-1-onto→(𝒫 𝒫 𝐵𝑚 𝐵))

Theoremneicvgnvo 38233* If neighborhood and convergent functions are related by operator 𝐻, it is its own converse function. (Contributed by RP, 11-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛𝑚 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛𝑜))))))    &   𝐷 = (𝑃𝐵)    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   𝐺 = (𝐵𝑂𝒫 𝐵)    &   𝐻 = (𝐹 ∘ (𝐷𝐺))    &   (𝜑𝑁𝐻𝑀)       (𝜑𝐻 = 𝐻)

Theoremneicvgnvor 38234* If neighborhood and convergent functions are related by operator 𝐻, the relationship holds with the functions swapped. (Contributed by RP, 11-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛𝑚 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛𝑜))))))    &   𝐷 = (𝑃𝐵)    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   𝐺 = (𝐵𝑂𝒫 𝐵)    &   𝐻 = (𝐹 ∘ (𝐷𝐺))    &   (𝜑𝑁𝐻𝑀)       (𝜑𝑀𝐻𝑁)

Theoremneicvgmex 38235* If the neighborhoods and convergents functions are related, the convergents function exists. (Contributed by RP, 27-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛𝑚 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛𝑜))))))    &   𝐷 = (𝑃𝐵)    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   𝐺 = (𝐵𝑂𝒫 𝐵)    &   𝐻 = (𝐹 ∘ (𝐷𝐺))    &   (𝜑𝑁𝐻𝑀)       (𝜑𝑀 ∈ (𝒫 𝒫 𝐵𝑚 𝐵))

Theoremneicvgnex 38236* If the neighborhoods and convergents functions are related, the neighborhoods function exists. (Contributed by RP, 27-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛𝑚 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛𝑜))))))    &   𝐷 = (𝑃𝐵)    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   𝐺 = (𝐵𝑂𝒫 𝐵)    &   𝐻 = (𝐹 ∘ (𝐷𝐺))    &   (𝜑𝑁𝐻𝑀)       (𝜑𝑁 ∈ (𝒫 𝒫 𝐵𝑚 𝐵))

Theoremneicvgel1 38237* A subset being an element of a neighborhood of a point is equivalent to the complement of that subset not being a element of the convergent of that point. (Contributed by RP, 12-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛𝑚 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛𝑜))))))    &   𝐷 = (𝑃𝐵)    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   𝐺 = (𝐵𝑂𝒫 𝐵)    &   𝐻 = (𝐹 ∘ (𝐷𝐺))    &   (𝜑𝑁𝐻𝑀)    &   (𝜑𝑋𝐵)    &   (𝜑𝑆 ∈ 𝒫 𝐵)       (𝜑 → (𝑆 ∈ (𝑁𝑋) ↔ ¬ (𝐵𝑆) ∈ (𝑀𝑋)))

Theoremneicvgel2 38238* The complement of a subset being an element of a neighborhood at a point is equivalent to that subset not being a element of the convergent at that point. (Contributed by RP, 12-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛𝑚 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛𝑜))))))    &   𝐷 = (𝑃𝐵)    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   𝐺 = (𝐵𝑂𝒫 𝐵)    &   𝐻 = (𝐹 ∘ (𝐷𝐺))    &   (𝜑𝑁𝐻𝑀)    &   (𝜑𝑋𝐵)    &   (𝜑𝑆 ∈ 𝒫 𝐵)       (𝜑 → ((𝐵𝑆) ∈ (𝑁𝑋) ↔ ¬ 𝑆 ∈ (𝑀𝑋)))

Theoremneicvgfv 38239* The value of the neighborhoods (convergents) in terms of the the convergents (neighborhoods) function. (Contributed by RP, 27-Jun-2021.)
𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗𝑚 𝑖) ↦ (𝑙𝑗 ↦ {𝑚𝑖𝑙 ∈ (𝑘𝑚)})))    &   𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛𝑚 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛𝑜))))))    &   𝐷 = (𝑃𝐵)    &   𝐹 = (𝒫 𝐵𝑂𝐵)    &   𝐺 = (𝐵𝑂𝒫 𝐵)    &   𝐻 = (𝐹 ∘ (𝐷𝐺))    &   (𝜑𝑁𝐻𝑀)    &   (𝜑𝑋𝐵)       (𝜑 → (𝑁𝑋) = {𝑠 ∈ 𝒫 𝐵 ∣ ¬ (𝐵𝑠) ∈ (𝑀𝑋)})

Theoremntrrn 38240 The range of the interior function of a topology a subset of the open sets of the topology. (Contributed by RP, 22-Apr-2021.)
𝑋 = 𝐽    &   𝐼 = (int‘𝐽)       (𝐽 ∈ Top → ran 𝐼𝐽)

Theoremntrf 38241 The interior function of a topology is a map from the powerset of the base set to the open sets of the topology. (Contributed by RP, 22-Apr-2021.)
𝑋 = 𝐽    &   𝐼 = (int‘𝐽)       (𝐽 ∈ Top → 𝐼:𝒫 𝑋𝐽)

Theoremntrf2 38242 The interior function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021.)
𝑋 = 𝐽    &   𝐼 = (int‘𝐽)       (𝐽 ∈ Top → 𝐼:𝒫 𝑋⟶𝒫 𝑋)

Theoremntrelmap 38243 The interior function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021.)
𝑋 = 𝐽    &   𝐼 = (int‘𝐽)       (𝐽 ∈ Top → 𝐼 ∈ (𝒫 𝑋𝑚 𝒫 𝑋))

Theoremclsf2 38244 The closure function is a map from the powerset of the base set to itself. This is less precise than clsf 20833. (Contributed by RP, 22-Apr-2021.)
𝑋 = 𝐽    &   𝐾 = (cls‘𝐽)       (𝐽 ∈ Top → 𝐾:𝒫 𝑋⟶𝒫 𝑋)

Theoremclselmap 38245 The closure function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021.)
𝑋 = 𝐽    &   𝐾 = (cls‘𝐽)       (𝐽 ∈ Top → 𝐾 ∈ (𝒫 𝑋𝑚 𝒫 𝑋))

Theoremdssmapntrcls 38246* The interior and closure operators on a topology are duals of each other. See also kur14lem2 31163. (Contributed by RP, 21-Apr-2021.)
𝑋 = 𝐽    &   𝐾 = (cls‘𝐽)    &   𝐼 = (int‘𝐽)    &   𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠))))))    &   𝐷 = (𝑂𝑋)       (𝐽 ∈ Top → 𝐼 = (𝐷𝐾))

Theoremdssmapclsntr 38247* The closure and interior operators on a topology are duals of each other. See also kur14lem2 31163. (Contributed by RP, 22-Apr-2021.)
𝑋 = 𝐽    &   𝐾 = (cls‘𝐽)    &   𝐼 = (int‘𝐽)    &   𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠))))))    &   𝐷 = (𝑂𝑋)       (𝐽 ∈ Top → 𝐾 = (𝐷𝐼))

20.26.4.3  Generic Neighborhood Spaces

Any neighborhood space is an open set topology and any open set topology is a neighborhood space. Seifert And Threlfall define a generic neighborhood space which is a superset of what is now generally used and related concepts and the following will show that those definitions apply to elements of Top.

Seifert And Threlfall do not allow neighborhood spaces on the empty set while sn0top 20784 is an example of a topology with an empty base set. This divergence is unlikely to pose serious problems.

Theoremgneispa 38248* Each point 𝑝 of the neighborhood space has at least one neighborhood; each neighborhood of 𝑝 contains 𝑝. Axiom A of Seifert And Threlfall. (Contributed by RP, 5-Apr-2021.)
𝑋 = 𝐽       (𝐽 ∈ Top → ∀𝑝𝑋 (((nei‘𝐽)‘{𝑝}) ≠ ∅ ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝑝})𝑝𝑛))

Theoremgneispb 38249* Given a neighborhood 𝑁 of 𝑃, each subset of the neighborhood space containing this neighborhood is also a neighborhood of 𝑃. Axiom B of Seifert And Threlfall. (Contributed by RP, 5-Apr-2021.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑃𝑋𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ∀𝑠 ∈ 𝒫 𝑋(𝑁𝑠𝑠 ∈ ((nei‘𝐽)‘{𝑃})))

Theoremgneispace2 38250* The predicate that 𝐹 is a (generic) Seifert And Threlfall neighborhood space. (Contributed by RP, 15-Apr-2021.)
𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓𝑛 ∈ (𝑓𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛𝑠𝑠 ∈ (𝑓𝑝))))}       (𝐹𝑉 → (𝐹𝐴 ↔ (𝐹:dom 𝐹⟶(𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))))

Theoremgneispace3 38251* The predicate that 𝐹 is a (generic) Seifert And Threlfall neighborhood space. (Contributed by RP, 15-Apr-2021.)
𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓𝑛 ∈ (𝑓𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛𝑠𝑠 ∈ (𝑓𝑝))))}       (𝐹𝑉 → (𝐹𝐴 ↔ ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))))

Theoremgneispace 38252* The predicate that 𝐹 is a (generic) Seifert And Threlfall neighborhood space. (Contributed by RP, 14-Apr-2021.)
𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓𝑛 ∈ (𝑓𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛𝑠𝑠 ∈ (𝑓𝑝))))}       (𝐹𝑉 → (𝐹𝐴 ↔ (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))))

Theoremgneispacef 38253* A generic neighborhood space is a function with a range that is a subset of the powerset of the powerset of its domain. (Contributed by RP, 15-Apr-2021.)
𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓𝑛 ∈ (𝑓𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛𝑠𝑠 ∈ (𝑓𝑝))))}       (𝐹𝐴𝐹:dom 𝐹⟶(𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))

Theoremgneispacef2 38254* A generic neighborhood space is a function with a range that is a subset of the powerset of the powerset of its domain. (Contributed by RP, 15-Apr-2021.)
𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓𝑛 ∈ (𝑓𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛𝑠𝑠 ∈ (𝑓𝑝))))}       (𝐹𝐴𝐹:dom 𝐹⟶𝒫 𝒫 dom 𝐹)

Theoremgneispacefun 38255* A generic neighborhood space is a function. (Contributed by RP, 15-Apr-2021.)
𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓𝑛 ∈ (𝑓𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛𝑠𝑠 ∈ (𝑓𝑝))))}       (𝐹𝐴 → Fun 𝐹)

Theoremgneispacern 38256* A generic neighborhood space has a range that is a subset of the powerset of the powerset of its domain. (Contributed by RP, 15-Apr-2021.)
𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓𝑛 ∈ (𝑓𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛𝑠𝑠 ∈ (𝑓𝑝))))}       (𝐹𝐴 → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))

Theoremgneispacern2 38257* A generic neighborhood space has a range that is a subset of the powerset of the powerset of its domain. (Contributed by RP, 15-Apr-2021.)
𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓𝑛 ∈ (𝑓𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛𝑠𝑠 ∈ (𝑓𝑝))))}       (𝐹𝐴 → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹)

Theoremgneispace0nelrn 38258* A generic neighborhood space has a non-empty set of neighborhoods for every point in its domain. (Contributed by RP, 15-Apr-2021.)
𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓𝑛 ∈ (𝑓𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛𝑠𝑠 ∈ (𝑓𝑝))))}       (𝐹𝐴 → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅)

Theoremgneispace0nelrn2 38259* A generic neighborhood space has a non-empty set of neighborhoods for every point in its domain. (Contributed by RP, 15-Apr-2021.)
𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓𝑛 ∈ (𝑓𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛𝑠𝑠 ∈ (𝑓𝑝))))}       ((𝐹𝐴𝑃 ∈ dom 𝐹) → (𝐹𝑃) ≠ ∅)

Theoremgneispace0nelrn3 38260* A generic neighborhood space has a non-empty set of neighborhoods for every point in its domain. (Contributed by RP, 15-Apr-2021.)
𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓𝑛 ∈ (𝑓𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛𝑠𝑠 ∈ (𝑓𝑝))))}       (𝐹𝐴 → ¬ ∅ ∈ ran 𝐹)

Theoremgneispaceel 38261* Every neighborhood of a point in a generic neighborhood space contains that point. (Contributed by RP, 15-Apr-2021.)
𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓𝑛 ∈ (𝑓𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛𝑠𝑠 ∈ (𝑓𝑝))))}       (𝐹𝐴 → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)𝑝𝑛)

Theoremgneispaceel2 38262* Every neighborhood of a point in a generic neighborhood space contains that point. (Contributed by RP, 15-Apr-2021.)
𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓𝑛 ∈ (𝑓𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛𝑠𝑠 ∈ (𝑓𝑝))))}       ((𝐹𝐴𝑃 ∈ dom 𝐹𝑁 ∈ (𝐹𝑃)) → 𝑃𝑁)

Theoremgneispacess 38263* All supersets of a neighborhood of a point (limited to the domain of the neighborhood space) are also neighborhoods of that point. (Contributed by RP, 15-Apr-2021.)
𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓𝑛 ∈ (𝑓𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛𝑠𝑠 ∈ (𝑓𝑝))))}       (𝐹𝐴 → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))

Theoremgneispacess2 38264* All supersets of a neighborhood of a point (limited to the domain of the neighborhood space) are also neighborhoods of that point. (Contributed by RP, 15-Apr-2021.)
𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓𝑛 ∈ (𝑓𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛𝑠𝑠 ∈ (𝑓𝑝))))}       (((𝐹𝐴𝑃 ∈ dom 𝐹) ∧ (𝑁 ∈ (𝐹𝑃) ∧ 𝑆 ∈ 𝒫 dom 𝐹𝑁𝑆)) → 𝑆 ∈ (𝐹𝑃))

20.26.5  Exploring Higher Homotopy via Kerodon

See https://kerodon.net/ for a work in progress by Jacob Lurie.

20.26.5.1  Simplicial Sets

See https://kerodon.net/tag/0004 for introduction to the topological simplex of dimension 𝑁.

Theoremk0004lem1 38265 Application of ssin 3827 to range of a function. (Contributed by RP, 1-Apr-2021.)
(𝐷 = (𝐵𝐶) → ((𝐹:𝐴𝐵 ∧ (𝐹𝐴) ⊆ 𝐶) ↔ 𝐹:𝐴𝐷))

Theoremk0004lem2 38266 A mapping with a particular restricted range is also a mapping to that range. (Contributed by RP, 1-Apr-2021.)
((𝐴𝑈𝐵𝑉𝐶𝐵) → ((𝐹 ∈ (𝐵𝑚 𝐴) ∧ (𝐹𝐴) ⊆ 𝐶) ↔ 𝐹 ∈ (𝐶𝑚 𝐴)))

Theoremk0004lem3 38267 When the value of a mapping on a singleton is known, the mapping is a a completely known singleton. (Contributed by RP, 2-Apr-2021.)
((𝐴𝑈𝐵𝑉𝐶𝐵) → ((𝐹 ∈ (𝐵𝑚 {𝐴}) ∧ (𝐹𝐴) = 𝐶) ↔ 𝐹 = {⟨𝐴, 𝐶⟩}))

Theoremk0004val 38268* The topological simplex of dimension 𝑁 is the set of real vectors where the components are nonnegative and sum to 1. (Contributed by RP, 29-Mar-2021.)
𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑𝑚 (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡𝑘) = 1})       (𝑁 ∈ ℕ0 → (𝐴𝑁) = {𝑡 ∈ ((0[,]1) ↑𝑚 (1...(𝑁 + 1))) ∣ Σ𝑘 ∈ (1...(𝑁 + 1))(𝑡𝑘) = 1})

Theoremk0004ss1 38269* The topological simplex of dimension 𝑁 is a subset of the real vectors of dimension (𝑁 + 1). (Contributed by RP, 29-Mar-2021.)
𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑𝑚 (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡𝑘) = 1})       (𝑁 ∈ ℕ0 → (𝐴𝑁) ⊆ (ℝ ↑𝑚 (1...(𝑁 + 1))))

Theoremk0004ss2 38270* The topological simplex of dimension 𝑁 is a subset of the base set of a real vector space of dimension (𝑁 + 1). (Contributed by RP, 29-Mar-2021.)
𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑𝑚 (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡𝑘) = 1})       (𝑁 ∈ ℕ0 → (𝐴𝑁) ⊆ (Base‘(ℝ^‘(1...(𝑁 + 1)))))

Theoremk0004ss3 38271* The topological simplex of dimension 𝑁 is a subset of the base set of Euclidean space of dimension (𝑁 + 1). (Contributed by RP, 29-Mar-2021.)
𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑𝑚 (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡𝑘) = 1})       (𝑁 ∈ ℕ0 → (𝐴𝑁) ⊆ (Base‘(𝔼hil‘(𝑁 + 1))))

Theoremk0004val0 38272* The topological simplex of dimension 0 is a singleton. (Contributed by RP, 2-Apr-2021.)
𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑𝑚 (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡𝑘) = 1})       (𝐴‘0) = {{⟨1, 1⟩}}

20.27  Mathbox for Stanislas Polu

Theoreminductionexd 38273 Simple induction example. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝑁 ∈ ℕ → 3 ∥ ((4↑𝑁) + 5))

20.27.1  IMO Problems

20.27.1.1  IMO 1972 B2

Theoremwwlemuld 38274 Natural deduction form of lemul2d 11901. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ)    &   (𝜑 → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))    &   (𝜑 → 0 < 𝐶)       (𝜑𝐴𝐵)

Theoremleeq1d 38275 Specialization of breq1d 4654 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑𝐴𝐶)    &   (𝜑𝐴 = 𝐵)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ)       (𝜑𝐵𝐶)

Theoremleeq2d 38276 Specialization of breq2d 4656 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑𝐴𝐶)    &   (𝜑𝐶 = 𝐷)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ)       (𝜑𝐴𝐷)

Theoremabsmulrposd 38277 Specialization of absmuld with absidd 14142. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑 → 0 ≤ 𝐴)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)       (𝜑 → (abs‘(𝐴 · 𝐵)) = (𝐴 · (abs‘𝐵)))

Theoremimadisjld 38278 Natural dduction form of one side of imadisj 5472. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑 → (dom 𝐴𝐵) = ∅)       (𝜑 → (𝐴𝐵) = ∅)

Theoremimadisjlnd 38279 Natural deduction form of one negated side of imadisj 5472. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑 → (dom 𝐴𝐵) ≠ ∅)       (𝜑 → (𝐴𝐵) ≠ ∅)

Theoremwnefimgd 38280 The image of a mapping from A is non empty if A is non empty. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑𝐴 ≠ ∅)    &   (𝜑𝐹:𝐴𝐵)       (𝜑 → (𝐹𝐴) ≠ ∅)

Theoremfco2d 38281 Natural deduction form of fco2 6046. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑𝐺:𝐴𝐵)    &   (𝜑 → (𝐹𝐵):𝐵𝐶)       (𝜑 → (𝐹𝐺):𝐴𝐶)

Theoremfvco3d 38282 Natural deduction form of fvco3 6262. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑𝐺:𝐴𝐵)    &   (𝜑𝐶𝐴)       (𝜑 → ((𝐹𝐺)‘𝐶) = (𝐹‘(𝐺𝐶)))

Theoremwfximgfd 38283 The value of a function on its domain is in the image of the function. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑𝐶𝐴)    &   (𝜑𝐹:𝐴𝐵)       (𝜑 → (𝐹𝐶) ∈ (𝐹𝐴))

Theoremextoimad 38284* If |f(x)| <= C for all x then it applies to all x in the image of |f(x)| (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑𝐹:ℝ⟶ℝ)    &   (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹𝑦)) ≤ 𝐶)       (𝜑 → ∀𝑥 ∈ (abs “ (𝐹 “ ℝ))𝑥𝐶)

Theoremimo72b2lem0 38285* Lemma for imo72b2 38295. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑𝐹:ℝ⟶ℝ)    &   (𝜑𝐺:ℝ⟶ℝ)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → ((𝐹‘(𝐴 + 𝐵)) + (𝐹‘(𝐴𝐵))) = (2 · ((𝐹𝐴) · (𝐺𝐵))))    &   (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹𝑦)) ≤ 1)       (𝜑 → ((abs‘(𝐹𝐴)) · (abs‘(𝐺𝐵))) ≤ sup((abs “ (𝐹 “ ℝ)), ℝ, < ))

Theoremsuprleubrd 38286* Natural deduction form of specialized suprleub 10974. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑𝐴 ⊆ ℝ)    &   (𝜑𝐴 ≠ ∅)    &   (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → ∀𝑧𝐴 𝑧𝐵)       (𝜑 → sup(𝐴, ℝ, < ) ≤ 𝐵)

Theoremimo72b2lem2 38287* Lemma for imo72b2 38295. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑𝐹:ℝ⟶ℝ)    &   (𝜑𝐶 ∈ ℝ)    &   (𝜑 → ∀𝑧 ∈ ℝ (abs‘(𝐹𝑧)) ≤ 𝐶)       (𝜑 → sup((abs “ (𝐹 “ ℝ)), ℝ, < ) ≤ 𝐶)

Theoremsyldbl2 38288 Stacked hypotheseis implies goal. (Contributed by Stanislas Polu, 9-Mar-2020.)
((𝜑𝜓) → (𝜓𝜃))       ((𝜑𝜓) → 𝜃)

Theoremfunfvima2d 38289 A function's value in a preimage belongs to the image. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑𝐹:𝐴𝐵)       ((𝜑𝑥𝐴) → (𝐹𝑥) ∈ (𝐹𝐴))

Theoremsuprlubrd 38290* Natural deduction form of specialized suprlub 10972. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑𝐴 ⊆ ℝ)    &   (𝜑𝐴 ≠ ∅)    &   (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → ∃𝑧𝐴 𝐵 < 𝑧)       (𝜑𝐵 < sup(𝐴, ℝ, < ))

Theoremimo72b2lem1 38291* Lemma for imo72b2 38295. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑𝐹:ℝ⟶ℝ)    &   (𝜑 → ∃𝑥 ∈ ℝ (𝐹𝑥) ≠ 0)    &   (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹𝑦)) ≤ 1)       (𝜑 → 0 < sup((abs “ (𝐹 “ ℝ)), ℝ, < ))

Theoremlemuldiv3d 38292 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑 → (𝐵 · 𝐴) ≤ 𝐶)    &   (𝜑 → 0 < 𝐴)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ)       (𝜑𝐵 ≤ (𝐶 / 𝐴))

Theoremlemuldiv4d 38293 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑𝐵 ≤ (𝐶 / 𝐴))    &   (𝜑 → 0 < 𝐴)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ)       (𝜑 → (𝐵 · 𝐴) ≤ 𝐶)

Theoremrspcdvinvd 38294* If something is true for all then it's true for some class. (Contributed by Stanislas Polu, 9-Mar-2020.)
((𝜑𝑥 = 𝐴) → (𝜓𝜒))    &   (𝜑𝐴𝐵)    &   (𝜑 → ∀𝑥𝐵 𝜓)       (𝜑𝜒)

Theoremimo72b2 38295* IMO 1972 B2. (14th International Mathemahics Olympiad in Poland, problem B2). (Contributed by Stanislas Polu, 9-Mar-2020.)
(𝜑𝐹:ℝ⟶ℝ)    &   (𝜑𝐺:ℝ⟶ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → ∀𝑢 ∈ ℝ ∀𝑣 ∈ ℝ ((𝐹‘(𝑢 + 𝑣)) + (𝐹‘(𝑢𝑣))) = (2 · ((𝐹𝑢) · (𝐺𝑣))))    &   (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹𝑦)) ≤ 1)    &   (𝜑 → ∃𝑥 ∈ ℝ (𝐹𝑥) ≠ 0)       (𝜑 → (abs‘(𝐺𝐵)) ≤ 1)

20.27.2  INT Inequalities Proof Generator

This section formalizes theorems necessary to reproduce the equality and inequality generator described in "Neural Theorem Proving on Inequality Problems" http://aitp-conference.org/2020/abstract/paper_18.pdf.

Other theorems required: 0red 10026 1red 10040 readdcld 10054 remulcld 10055 eqcomd 2626.

(𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ)    &   (𝜑𝐴 = 𝐵)       (𝜑 → (𝐵 + 𝐶) = (𝐶 + 𝐴))

(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ)    &   (𝜑𝐷 ∈ ℝ)    &   (𝜑𝐴 = 𝐵)       (𝜑 → (𝐵 + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + 𝐷))