P. 441 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

fsovfd 44001*

The operator, (𝐴𝑂𝐵), which maps between maps from one base set to subsets of the second to maps from the second base set to subsets of the first for base sets, 𝐴 and 𝐵, gives a function between two sets of functions. (Contributed by RP, 27-Apr-2021.)

⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐺 = (𝐴𝑂𝐵)    ⇒   ⊢ (𝜑 → 𝐺:(𝒫 𝐵 ↑_m 𝐴)⟶(𝒫 𝐴 ↑_m 𝐵))

Theorem

fsovcnvlem 44002*

The 𝑂 operator, which maps between maps from one base set to subsets of the second to maps from the second base set to subsets of the first for base sets, gives a family of functions that include their own inverse. (Contributed by RP, 27-Apr-2021.)

⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐺 = (𝐴𝑂𝐵)    &   ⊢ 𝐻 = (𝐵𝑂𝐴)    ⇒   ⊢ (𝜑 → (𝐻 ∘ 𝐺) = ( I ↾ (𝒫 𝐵 ↑_m 𝐴)))

Theorem

fsovcnvd 44003*

The value of the converse (𝐴𝑂𝐵) is (𝐵𝑂𝐴), where 𝑂 is the operator which maps between maps from one base set to subsets of the second to maps from the second base set to subsets of the first for base sets, gives a family of functions that include their own inverse. (Contributed by RP, 27-Apr-2021.)

⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐺 = (𝐴𝑂𝐵)    &   ⊢ 𝐻 = (𝐵𝑂𝐴)    ⇒   ⊢ (𝜑 → ^◡𝐺 = 𝐻)

Theorem

fsovcnvfvd 44004*

The value of the converse of (𝐴𝑂𝐵), where 𝑂 is the operator which maps between maps from one base set to subsets of the second to maps from the second base set to subsets of the first for base sets, evaluated at function 𝐹. (Contributed by RP, 27-Apr-2021.)

⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐺 = (𝐴𝑂𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝒫 𝐴 ↑_m 𝐵))    ⇒   ⊢ (𝜑 → (^◡𝐺‘𝐹) = (𝑦 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ 𝑦 ∈ (𝐹‘𝑥)}))

Theorem

fsovf1od 44005*

The value of (𝐴𝑂𝐵) is a bijection, where 𝑂 is the operator which maps between maps from one base set to subsets of the second to maps from the second base set to subsets of the first for base sets. (Contributed by RP, 27-Apr-2021.)

⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐺 = (𝐴𝑂𝐵)    ⇒   ⊢ (𝜑 → 𝐺:(𝒫 𝐵 ↑_m 𝐴)–1-1-onto→(𝒫 𝐴 ↑_m 𝐵))

Theorem

dssmapfvd 44006*

Value of the duality operator for self-mappings of subsets of a base set, 𝐵. (Contributed by RP, 19-Apr-2021.)

⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐷 = (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))))

Theorem

dssmapfv2d 44007*

Value of the duality operator for self-mappings of subsets of a base set, 𝐵 when applied to function 𝐹. (Contributed by RP, 19-Apr-2021.)

⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))    &   ⊢ 𝐺 = (𝐷‘𝐹)    ⇒   ⊢ (𝜑 → 𝐺 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝐹‘(𝐵 ∖ 𝑠)))))

Theorem

dssmapfv3d 44008*

Value of the duality operator for self-mappings of subsets of a base set, 𝐵 when applied to function 𝐹 and subset 𝑆. (Contributed by RP, 19-Apr-2021.)

⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))    &   ⊢ 𝐺 = (𝐷‘𝐹)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    &   ⊢ 𝑇 = (𝐺‘𝑆)    ⇒   ⊢ (𝜑 → 𝑇 = (𝐵 ∖ (𝐹‘(𝐵 ∖ 𝑆))))

Theorem

dssmapnvod 44009*

For any base set 𝐵 the duality operator for self-mappings of subsets of that base set is its own inverse, an involution. (Contributed by RP, 20-Apr-2021.)

⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ^◡𝐷 = 𝐷)

Theorem

dssmapf1od 44010*

For any base set 𝐵 the duality operator for self-mappings of subsets of that base set is one-to-one and onto. (Contributed by RP, 21-Apr-2021.)

⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐷:(𝒫 𝐵 ↑_m 𝒫 𝐵)–1-1-onto→(𝒫 𝐵 ↑_m 𝒫 𝐵))

Theorem

dssmap2d 44011*

For any base set 𝐵 the duality operator for self-mappings of subsets of that base set when composed with itself is the restricted identity operator. (Contributed by RP, 21-Apr-2021.)

⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐷 ∘ 𝐷) = ( I ↾ (𝒫 𝐵 ↑_m 𝒫 𝐵)))

21.36.7.2  Generic Pseudoclosure Spaces, Pseudointerior Spaces, and Pseudoneighborhoods

For any base set, 𝐵, an arbitrary mapping of subsets to subsets can be called a pseudoclosure (pseudointerior) function, 𝐾, with its dual of a pseudointerior (pseudoclosure), 𝐼, related by the involution in dssmapfvd 44006. As 𝐾 gains properties of the closure (interior) function of a topology on 𝐵, so does its dual gain corresponding properties of the interior (closure) function of that topology.

As (𝒫 𝐵 ↑_m 𝒫 𝐵) ≈ (𝒫 𝒫 𝐵 ↑_m 𝐵) there is also a natural isomorphism which maps from 𝐼 to 𝑁 (and likewise for 𝐾 and 𝑀, introduced below) which identically gains the properties of the neighborhood function of a topology (modified and restricted to operate on single points). A function dual to 𝑁, which Stadler and Stadler refer to as a convergent function, is represented by 𝑀 in this section.

Based on this and the early treatment of topology in Seifert and Threlfall, it seems reasonable to define a pseudotopology as defined in terms of its base set and one of these functions with theorems treating the equivalence of the other definitions and adding topological structure if enough properties hold true.

	Neighborhoods		Interior		Closure		Convergents	Theorems
Functions	𝑁 ∈ (𝒫 𝒫 𝐵 ↑m 𝐵)		𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)		𝐾 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)		𝑀 ∈ (𝒫 𝒫 𝐵 ↑m 𝐵)
Correspondences (assuming (𝑋 ∈ 𝐵 ∧ 𝑆 ∈ 𝒫 𝐵))	𝑆 ∈ (𝑁‘𝑋)	↔	𝑋 ∈ (𝐼‘𝑆)	↔	¬ 𝑋 ∈ (𝐾‘(𝐵 ∖ 𝑆))	↔	¬ (𝐵 ∖ 𝑆) ∈ (𝑀‘𝑋)	ntrclselnel1 44046, ntrneiel 44070, neicvgel1 44108
	¬ (𝐵 ∖ 𝑆) ∈ (𝑁‘𝑋)	↔	¬ 𝑋 ∈ (𝐼‘(𝐵 ∖ 𝑆))	↔	𝑋 ∈ (𝐾‘𝑆)	↔	𝑆 ∈ (𝑀‘𝑋)
Neighborhoods	(𝑁‘𝑋)	=	{𝑠 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ (𝐼‘𝑠)}	=	{𝑠 ∈ 𝒫 𝐵 ∣ ¬ 𝑋 ∈ (𝐾‘(𝐵 ∖ 𝑠))}	=	{𝑠 ∈ 𝒫 𝐵 ∣ ¬ (𝐵 ∖ 𝑠) ∈ (𝑀‘𝑋)}	ntrneifv3 44071, clsneifv3 44099, neicvgfv 44110
Interior	{𝑥 ∈ 𝐵 ∣ 𝑆 ∈ (𝑁‘𝑥)}	=	(𝐼‘𝑆)	=	(𝐵 ∖ (𝐾‘(𝐵 ∖ 𝑆)))	=	{𝑥 ∈ 𝐵 ∣ ¬ (𝐵 ∖ 𝑆) ∈ (𝑀‘𝑥)}	ntrneifv4 44074, ntrclsfv 44048, clsneifv4 44100
Closure	{𝑥 ∈ 𝐵 ∣ ¬ (𝐵 ∖ 𝑆) ∈ (𝑁‘𝑥)}	=	(𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑆)))	=	(𝐾‘𝑆)	=	{𝑥 ∈ 𝐵 ∣ 𝑆 ∈ (𝑀‘𝑥)}	clsneifv4 44100, ntrclsfv 44048, ntrneifv4 44074
Convergents	{𝑠 ∈ 𝒫 𝐵 ∣ ¬ (𝐵 ∖ 𝑠) ∈ (𝑁‘𝑋)}	=	{𝑠 ∈ 𝒫 𝐵 ∣ ¬ 𝑋 ∈ (𝐼‘(𝐵 ∖ 𝑠))}	=	{𝑠 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ (𝐾‘𝑠)}	=	(𝑀‘𝑋)	neicvgfv 44110, clsneifv3 44099, ntrneifv3 44071

We have the following table of equivalences to axioms largely established by Kuratowski. In the formulas in this table, to reduce the width of the columns, if any of the variables 𝑥, 𝑠, or 𝑡 are used, then they are implicitly universally quantified and 𝑥 (respectively 𝑠 and 𝑡) ranges over 𝐵 (respectively 𝒫 𝐵 and 𝒫 𝐵).

Assuming a prefix of: ∀𝑥 ∈ 𝐵∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵	Neighborhoods	Interior	Closure	Convergents	Equivalence Theorems
K0' Neighborhoods are nonempty.	(𝑁‘𝑥) ≠ ∅	∃𝑢 ∈ 𝒫 𝐵𝑥 ∈ (𝐼‘𝑢)	∃𝑢 ∈ 𝒫 𝐵¬ 𝑥 ∈ (𝐾‘𝑢)	(𝑀‘𝑥) ≠ 𝒫 𝐵	ntrclsneine0 44054, ntrneineine0 44076, ntrneineine1 44077
KA' No neighborhood is equal to the full powerset.	(𝑁‘𝑥) ≠ 𝒫 𝐵	∃𝑢 ∈ 𝒫 𝐵¬ 𝑥 ∈ (𝐼‘𝑢)	∃𝑢 ∈ 𝒫 𝐵𝑥 ∈ (𝐾‘𝑢)	(𝑀‘𝑥) ≠ ∅	ntrclsneine0 44054, ntrneineine0 44076, ntrneineine1 44077
K0 Preservation of the Nullary Union of Closures	𝐵 ∈ (𝑁‘𝑥)	(𝐼‘𝐵) = 𝐵	(𝐾‘∅) = ∅	¬ ∅ ∈ (𝑀‘𝑥)	ntrclscls00 44055, ntrneicls00 44078, ntrneicls11 44079
KA Preservation of the Nullary Union of Interiors	¬ ∅ ∈ (𝑁‘𝑥)	(𝐼‘∅) = ∅	(𝐾‘𝐵) = 𝐵	𝐵 ∈ (𝑀‘𝑥)	ntrclscls00 44055, ntrneicls00 44078, ntrneicls11 44079
K1 Isotonic Montonic	((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝑡) → 𝑡 ∈ (𝑁‘𝑥))	(𝑠 ⊆ 𝑡 → (𝐼‘𝑠) ⊆ (𝐼‘𝑡)) — or — ((𝐼‘𝑠) ∪ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∪ 𝑡)) — or — (𝐼‘(𝑠 ∩ 𝑡)) ⊆ ((𝐼‘𝑠) ∩ (𝐼‘𝑡))	(𝑠 ⊆ 𝑡 → (𝐾‘𝑠) ⊆ (𝐾‘𝑡)) — or — ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) ⊆ (𝐾‘(𝑠 ∪ 𝑡)) — or — (𝐾‘(𝑠 ∩ 𝑡)) ⊆ ((𝐾‘𝑠) ∩ (𝐾‘𝑡))	((𝑠 ∈ (𝑀‘𝑥) ∧ 𝑠 ⊆ 𝑡) → 𝑡 ∈ (𝑀‘𝑥))	isotone1 44037, isotone2 44038, ntrclsiso 44056, ntrneiiso 44080
K2 Closure is Expansive	(𝑠 ∈ (𝑁‘𝑥) → 𝑥 ∈ 𝑠)	(𝐼‘𝑠) ⊆ 𝑠	𝑠 ⊆ (𝐾‘𝑠)	(𝑥 ∈ 𝑠 → 𝑠 ∈ (𝑀‘𝑥))	ntrclsk2 44057, ntrneik2 44081, ntrneix2 44082
KB Non-disjoint Neighborhoods	((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅)	((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅)	((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)	((𝑠 ∪ 𝑡) = 𝐵 → (𝑠 ∈ (𝑀‘𝑥) ∨ 𝑡 ∈ (𝑀‘𝑥)))	ntrclskb 44058, ntrneikb 44083, ntrneixb 44084
K3 Closure is Sub-linear	((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥))	((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡))	(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))	((𝑠 ∪ 𝑡) ∈ (𝑀‘𝑥) → (𝑠 ∈ (𝑀‘𝑥) ∨ 𝑡 ∈ (𝑀‘𝑥)))	ntrclsk3 44059, ntrneik3 44085, ntrneix3 44086
K13 Closure is finitely linear	((𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)))	(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡))	(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))	((𝑠 ∪ 𝑡) ∈ (𝑀‘𝑥) ↔ (𝑠 ∈ (𝑀‘𝑥) ∨ 𝑡 ∈ (𝑀‘𝑥)))	ntrclsk13 44060, ntrneik13 44087, ntrneix13 44088
K4 Closure is idempotent	(𝑠 ∈ (𝑁‘𝑥) ↔ ∃𝑢 ∈ (𝑁‘𝑥)∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑠 ∈ (𝑁‘𝑦)))	(𝐼‘(𝐼‘𝑠)) = (𝐼‘𝑠)	(𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠)	(𝑠 ∈ (𝑀‘𝑥) ↔ ∃𝑢 ∈ (𝑀‘𝑥)∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑠 ∈ (𝑀‘𝑦)))	ntrclsk4 44061, ntrneik4 44090

Using these properties as axiomic constraints on the functions, certain collections of them give rise to named spaces.

Space	Foundational Axioms	Derived Axioms	Theorems
Csázár Generalized Neighborhood Space	K2	KA', KA, KB	ntrk2imkb 44026, ntrkbimka 44027, neik0imk0p 44025
Min Strong Generalized Neighborhood Space	K2, K3	KA', KA, KB	ntrk2imkb 44026, ntrkbimka 44027, neik0imk0p 44025
Gniłka Extended Topology	K0', K1	K0	neik0pk1imk0 44036
Brissaud Space	K0, K2	K0', KA', KA, KB	neik0imk0p 44025, ntrk2imkb 44026, ntrkbimka 44027
Neighborhood Space	K0', K1, K2	K0, KA', KA, KB	neik0pk1imk0 44036, ntrk2imkb 44026, ntrkbimka 44027, neik0imk0p 44025
Davey and Priestley Intersection Structure	K1, K4
Moore Closure Space	K1, K2, K4	KA', KA, KB	ntrk2imkb 44026, ntrkbimka 44027, neik0imk0p 44025
Convex Closure Space	K0', K1, K2, K4	K0, KA', KA, KB	neik0pk1imk0 44036, ntrk2imkb 44026, ntrkbimka 44027, neik0imk0p 44025
Smyth Neighborhood Space	K0', K13	K0, K1, K3	neik0pk1imk0 44036, ntrk1k3eqk13 44039
Čech Closure Space Pretopological Space	K0', K2, K13	K0, K1, KA', KA, KB, K3	neik0pk1imk0 44036, ntrk2imkb 44026, ntrkbimka 44027, neik0imk0p 44025, ntrk1k3eqk13 44039
Topological Space	K0', K2, K13, K4	K0, K1, KA', KA, KB, K3	neik0pk1imk0 44036, ntrk2imkb 44026, ntrkbimka 44027, neik0imk0p 44025, ntrk1k3eqk13 44039
Alexandroff Space	K0', K2, K5	K0, K1, KA', KA, KB, K3, K13	neik0pk1imk0 44036, ntrk2imkb 44026, ntrkbimka 44027, neik0imk0p 44025, ntrk1k3eqk13 44039, TBD
Alexandroff Topological Space	K0', K2, K4, K5	K0, K1, KA', KA, KB, K3, K13	neik0pk1imk0 44036, ntrk2imkb 44026, ntrkbimka 44027, neik0imk0p 44025, ntrk1k3eqk13 44039, TBD

Theorem

or3or 44012

Decompose disjunction into three cases. (Contributed by RP, 5-Jul-2021.)

⊢ ((𝜑 ∨ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓) ∨ (¬ 𝜑 ∧ 𝜓)))

Theorem

andi3or 44013

Distribute over triple disjunction. (Contributed by RP, 5-Jul-2021.)

⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒 ∨ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒) ∨ (𝜑 ∧ 𝜃)))

Theorem

uneqsn 44014

If a union of classes is equal to a singleton then at least one class is equal to the singleton while the other may be equal to the empty set. (Contributed by RP, 5-Jul-2021.)

⊢ ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))

Theorem

brfvimex 44015

If a binary relation holds and the relation is the value of a function, then the argument to that function is a set. (Contributed by RP, 22-May-2021.)

⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝑅 = (𝐹‘𝐶))    ⇒   ⊢ (𝜑 → 𝐶 ∈ V)

Theorem

brovmptimex 44016*

If a binary relation holds and the relation is the value of a binary operation built with maps-to, then the arguments to that operation are sets. (Contributed by RP, 22-May-2021.)

⊢ 𝐹 = (𝑥 ∈ 𝐸, 𝑦 ∈ 𝐺 ↦ 𝐻)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝑅 = (𝐶𝐹𝐷))    ⇒   ⊢ (𝜑 → (𝐶 ∈ V ∧ 𝐷 ∈ V))

Theorem

brovmptimex1 44017*

If a binary relation holds and the relation is the value of a binary operation built with maps-to, then the arguments to that operation are sets. (Contributed by RP, 22-May-2021.)

⊢ 𝐹 = (𝑥 ∈ 𝐸, 𝑦 ∈ 𝐺 ↦ 𝐻)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝑅 = (𝐶𝐹𝐷))    ⇒   ⊢ (𝜑 → 𝐶 ∈ V)

Theorem

brovmptimex2 44018*

If a binary relation holds and the relation is the value of a binary operation built with maps-to, then the arguments to that operation are sets. (Contributed by RP, 22-May-2021.)

⊢ 𝐹 = (𝑥 ∈ 𝐸, 𝑦 ∈ 𝐺 ↦ 𝐻)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝑅 = (𝐶𝐹𝐷))    ⇒   ⊢ (𝜑 → 𝐷 ∈ V)

Theorem

brcoffn 44019

Conditions allowing the decomposition of a binary relation. (Contributed by RP, 7-Jun-2021.)

⊢ (𝜑 → 𝐶 Fn 𝑌)    &   ⊢ (𝜑 → 𝐷:𝑋⟶𝑌)    &   ⊢ (𝜑 → 𝐴(𝐶 ∘ 𝐷)𝐵)    ⇒   ⊢ (𝜑 → (𝐴𝐷(𝐷‘𝐴) ∧ (𝐷‘𝐴)𝐶𝐵))

Theorem

brcofffn 44020

Conditions allowing the decomposition of a binary relation. (Contributed by RP, 8-Jun-2021.)

⊢ (𝜑 → 𝐶 Fn 𝑍)    &   ⊢ (𝜑 → 𝐷:𝑌⟶𝑍)    &   ⊢ (𝜑 → 𝐸:𝑋⟶𝑌)    &   ⊢ (𝜑 → 𝐴(𝐶 ∘ (𝐷 ∘ 𝐸))𝐵)    ⇒   ⊢ (𝜑 → (𝐴𝐸(𝐸‘𝐴) ∧ (𝐸‘𝐴)𝐷(𝐷‘(𝐸‘𝐴)) ∧ (𝐷‘(𝐸‘𝐴))𝐶𝐵))

Theorem

brco2f1o 44021

Conditions allowing the decomposition of a binary relation. (Contributed by RP, 8-Jun-2021.)

⊢ (𝜑 → 𝐶:𝑌–1-1-onto→𝑍)    &   ⊢ (𝜑 → 𝐷:𝑋–1-1-onto→𝑌)    &   ⊢ (𝜑 → 𝐴(𝐶 ∘ 𝐷)𝐵)    ⇒   ⊢ (𝜑 → ((^◡𝐶‘𝐵)𝐶𝐵 ∧ 𝐴𝐷(^◡𝐶‘𝐵)))

Theorem

brco3f1o 44022

Conditions allowing the decomposition of a binary relation. (Contributed by RP, 8-Jun-2021.)

⊢ (𝜑 → 𝐶:𝑌–1-1-onto→𝑍)    &   ⊢ (𝜑 → 𝐷:𝑋–1-1-onto→𝑌)    &   ⊢ (𝜑 → 𝐸:𝑊–1-1-onto→𝑋)    &   ⊢ (𝜑 → 𝐴(𝐶 ∘ (𝐷 ∘ 𝐸))𝐵)    ⇒   ⊢ (𝜑 → ((^◡𝐶‘𝐵)𝐶𝐵 ∧ (^◡𝐷‘(^◡𝐶‘𝐵))𝐷(^◡𝐶‘𝐵) ∧ 𝐴𝐸(^◡𝐷‘(^◡𝐶‘𝐵))))

Theorem

ntrclsbex 44023

If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then the base set exists. (Contributed by RP, 21-May-2021.)

⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → 𝐵 ∈ V)

Theorem

ntrclsrcomplex 44024

The relative complement of the class 𝑆 exists as a subset of the base set. (Contributed by RP, 25-Jun-2021.)

⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵)

Theorem

neik0imk0p 44025

Kuratowski's K0 axiom implies K0'. Neighborhood version. Also a proof the dual KA axiom implies KA' when considering the convergents. (Contributed by RP, 28-Jun-2021.)

⊢ (∀𝑥 ∈ 𝐵 𝐵 ∈ (𝑁‘𝑥) → ∀𝑥 ∈ 𝐵 (𝑁‘𝑥) ≠ ∅)

Theorem

ntrk2imkb 44026*

If an interior function is contracting, the interiors of disjoint sets are disjoint. Kuratowski's K2 axiom implies KB. Interior version. (Contributed by RP, 9-Jun-2021.)

⊢ (∀𝑠 ∈ 𝒫 𝐵(𝐼‘𝑠) ⊆ 𝑠 → ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅))

Theorem

ntrkbimka 44027*

If the interiors of disjoint sets are disjoint, then the interior of the empty set is the empty set. (Contributed by RP, 14-Jun-2021.)

⊢ (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) → (𝐼‘∅) = ∅)

Theorem

ntrk0kbimka 44028*

If the interiors of disjoint sets are disjoint and the interior of the base set is the base set, then the interior of the empty set is the empty set. Obsolete version of ntrkbimka 44027. (Contributed by RP, 12-Jun-2021.)

⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) → (((𝐼‘𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅)) → (𝐼‘∅) = ∅))

Theorem

clsk3nimkb 44029*

If the base set is not empty, axiom K3 does not imply KB. A concrete example with a pseudo-closure function of 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)) is given. (Contributed by RP, 16-Jun-2021.)

⊢ ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))

Theorem

clsk1indlem0 44030

The ansatz closure function (𝑟 ∈ 𝒫 3_o ↦ if(𝑟 = {∅}, {∅, 1_o}, 𝑟)) has the K0 property of preserving the nullary union. (Contributed by RP, 6-Jul-2021.)

⊢ 𝐾 = (𝑟 ∈ 𝒫 3_o ↦ if(𝑟 = {∅}, {∅, 1_o}, 𝑟))    ⇒   ⊢ (𝐾‘∅) = ∅

Theorem

clsk1indlem2 44031*

The ansatz closure function (𝑟 ∈ 𝒫 3_o ↦ if(𝑟 = {∅}, {∅, 1_o}, 𝑟)) has the K2 property of expanding. (Contributed by RP, 6-Jul-2021.)

⊢ 𝐾 = (𝑟 ∈ 𝒫 3_o ↦ if(𝑟 = {∅}, {∅, 1_o}, 𝑟))    ⇒   ⊢ ∀𝑠 ∈ 𝒫 3_o𝑠 ⊆ (𝐾‘𝑠)

Theorem

clsk1indlem3 44032*

The ansatz closure function (𝑟 ∈ 𝒫 3_o ↦ if(𝑟 = {∅}, {∅, 1_o}, 𝑟)) has the K3 property of being sub-linear. (Contributed by RP, 6-Jul-2021.)

⊢ 𝐾 = (𝑟 ∈ 𝒫 3_o ↦ if(𝑟 = {∅}, {∅, 1_o}, 𝑟))    ⇒   ⊢ ∀𝑠 ∈ 𝒫 3_o∀𝑡 ∈ 𝒫 3_o(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))

Theorem

clsk1indlem4 44033*

The ansatz closure function (𝑟 ∈ 𝒫 3_o ↦ if(𝑟 = {∅}, {∅, 1_o}, 𝑟)) has the K4 property of idempotence. (Contributed by RP, 6-Jul-2021.)

⊢ 𝐾 = (𝑟 ∈ 𝒫 3_o ↦ if(𝑟 = {∅}, {∅, 1_o}, 𝑟))    ⇒   ⊢ ∀𝑠 ∈ 𝒫 3_o(𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠)

Theorem

clsk1indlem1 44034*

The ansatz closure function (𝑟 ∈ 𝒫 3_o ↦ if(𝑟 = {∅}, {∅, 1_o}, 𝑟)) does not have the K1 property of isotony. (Contributed by RP, 6-Jul-2021.)

⊢ 𝐾 = (𝑟 ∈ 𝒫 3_o ↦ if(𝑟 = {∅}, {∅, 1_o}, 𝑟))    ⇒   ⊢ ∃𝑠 ∈ 𝒫 3_o∃𝑡 ∈ 𝒫 3_o(𝑠 ⊆ 𝑡 ∧ ¬ (𝐾‘𝑠) ⊆ (𝐾‘𝑡))

Theorem

clsk1independent 44035*

For generalized closure functions, property K1 (isotony) is independent of the properties K0, K2, K3, K4. This contradicts a claim which appears in preprints of Table 2 in Bärbel M. R. Stadler and Peter F. Stadler. "Generalized Topological Spaces in Evolutionary Theory and Combinatorial Chemistry." J. Chem. Inf. Comput. Sci., 42:577-585, 2002. Proceedings MCC 2001, Dubrovnik. The same table row implying K1 follows from the other four appears in the supplemental materials Bärbel M. R. Stadler and Peter F. Stadler. "Basic Properties of Closure Spaces" 2001 on page 12. (Contributed by RP, 5-Jul-2021.)

⊢ (𝜑 ↔ (𝑘‘∅) = ∅)    &   ⊢ (𝜓 ↔ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))    &   ⊢ (𝜒 ↔ ∀𝑠 ∈ 𝒫 𝑏𝑠 ⊆ (𝑘‘𝑠))    &   ⊢ (𝜃 ↔ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)))    &   ⊢ (𝜏 ↔ ∀𝑠 ∈ 𝒫 𝑏(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))    ⇒   ⊢ ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓)

Theorem

neik0pk1imk0 44036*

Kuratowski's K0' and K1 axioms imply K0. Neighborhood version. (Contributed by RP, 3-Jun-2021.)

⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ (𝒫 𝒫 𝐵 ↑_m 𝐵))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝑁‘𝑥) ≠ ∅)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝑡) → 𝑡 ∈ (𝑁‘𝑥)))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝐵 ∈ (𝑁‘𝑥))

Theorem

isotone1 44037*

Two different ways to say subset relation persists across applications of a function. (Contributed by RP, 31-May-2021.)

⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))

Theorem

isotone2 44038*

Two different ways to say subset relation persists across applications of a function. (Contributed by RP, 31-May-2021.)

⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝐹‘(𝑎 ∩ 𝑏)) ⊆ ((𝐹‘𝑎) ∩ (𝐹‘𝑏)))

Theorem

ntrk1k3eqk13 44039*

An interior function is both monotone and sub-linear if and only if it is finitely linear. (Contributed by RP, 18-Jun-2021.)

⊢ ((∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝑠 ⊆ 𝑡 → (𝐼‘𝑠) ⊆ (𝐼‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡))) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)))

Theorem

ntrclsf1o 44040*

If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator we may characterize the relation as part of a 1-to-1 onto function. (Contributed by RP, 29-May-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → 𝐷:(𝒫 𝐵 ↑_m 𝒫 𝐵)–1-1-onto→(𝒫 𝐵 ↑_m 𝒫 𝐵))

Theorem

ntrclsnvobr 44041*

If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then they are related the opposite way. (Contributed by RP, 21-May-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → 𝐾𝐷𝐼)

Theorem

ntrclsiex 44042*

If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then those functions are maps of subsets to subsets. (Contributed by RP, 21-May-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))

Theorem

ntrclskex 44043*

If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then those functions are maps of subsets to subsets. (Contributed by RP, 21-May-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))

Theorem

ntrclsfv1 44044*

If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then there is a functional relation between them (Contributed by RP, 28-May-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (𝐷‘𝐼) = 𝐾)

Theorem

ntrclsfv2 44045*

If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then there is a functional relation between them (Contributed by RP, 28-May-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (𝐷‘𝐾) = 𝐼)

Theorem

ntrclselnel1 44046*

If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then there is an equivalence between membership in the interior of a set and non-membership in the closure of the complement of the set. (Contributed by RP, 28-May-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐼‘𝑆) ↔ ¬ 𝑋 ∈ (𝐾‘(𝐵 ∖ 𝑆))))

Theorem

ntrclselnel2 44047*

If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then there is an equivalence between membership in interior of the complement of a set and non-membership in the closure of the set. (Contributed by RP, 28-May-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐼‘(𝐵 ∖ 𝑆)) ↔ ¬ 𝑋 ∈ (𝐾‘𝑆)))

Theorem

ntrclsfv 44048*

The value of the interior (closure) expressed in terms of the closure (interior). (Contributed by RP, 25-Jun-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑆) = (𝐵 ∖ (𝐾‘(𝐵 ∖ 𝑆))))

Theorem

ntrclsfveq1 44049*

If interior and closure functions are related then specific function values are complementary. (Contributed by RP, 27-Jun-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → ((𝐼‘𝑆) = 𝐶 ↔ (𝐾‘(𝐵 ∖ 𝑆)) = (𝐵 ∖ 𝐶)))

Theorem

ntrclsfveq2 44050*

If interior and closure functions are related then specific function values are complementary. (Contributed by RP, 27-Jun-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → ((𝐼‘(𝐵 ∖ 𝑆)) = 𝐶 ↔ (𝐾‘𝑆) = (𝐵 ∖ 𝐶)))

Theorem

ntrclsfveq 44051*

If interior and closure functions are related then equality of a pair of function values is equivalent to equality of a pair of the other function's values. (Contributed by RP, 27-Jun-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → ((𝐼‘𝑆) = (𝐼‘𝑇) ↔ (𝐾‘(𝐵 ∖ 𝑆)) = (𝐾‘(𝐵 ∖ 𝑇))))

Theorem

ntrclsss 44052*

If interior and closure functions are related then a subset relation of a pair of function values is equivalent to subset relation of a pair of the other function's values. (Contributed by RP, 27-Jun-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → ((𝐼‘𝑆) ⊆ (𝐼‘𝑇) ↔ (𝐾‘(𝐵 ∖ 𝑇)) ⊆ (𝐾‘(𝐵 ∖ 𝑆))))

Theorem

ntrclsneine0lem 44053*

If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then conditions equal to claiming that at least one (pseudo-)neighborbood of a particular point exists hold equally. (Contributed by RP, 21-May-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (∃𝑠 ∈ 𝒫 𝐵𝑋 ∈ (𝐼‘𝑠) ↔ ∃𝑠 ∈ 𝒫 𝐵 ¬ 𝑋 ∈ (𝐾‘𝑠)))

Theorem

ntrclsneine0 44054*

If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then conditions equal to claiming that for every point, at least one (pseudo-)neighborbood exists hold equally. (Contributed by RP, 21-May-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∃𝑠 ∈ 𝒫 𝐵𝑥 ∈ (𝐼‘𝑠) ↔ ∀𝑥 ∈ 𝐵 ∃𝑠 ∈ 𝒫 𝐵 ¬ 𝑥 ∈ (𝐾‘𝑠)))

Theorem

ntrclscls00 44055*

If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then conditions equal to claiming that the closure of the empty set is the empty set hold equally. (Contributed by RP, 1-Jun-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → ((𝐼‘𝐵) = 𝐵 ↔ (𝐾‘∅) = ∅))

Theorem

ntrclsiso 44056*

If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then conditions equal to claiming that either is isotonic hold equally. (Contributed by RP, 3-Jun-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝑠 ⊆ 𝑡 → (𝐼‘𝑠) ⊆ (𝐼‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝑠 ⊆ 𝑡 → (𝐾‘𝑠) ⊆ (𝐾‘𝑡))))

Theorem

ntrclsk2 44057*

An interior function is contracting if and only if the closure function is expansive. (Contributed by RP, 9-Jun-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵(𝐼‘𝑠) ⊆ 𝑠 ↔ ∀𝑠 ∈ 𝒫 𝐵𝑠 ⊆ (𝐾‘𝑠)))

Theorem

ntrclskb 44058*

The interiors of disjoint sets are disjoint if and only if the closures of sets that span the base set also span the base set. (Contributed by RP, 10-Jun-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))

Theorem

ntrclsk3 44059*

The intersection of interiors of a every pair is a subset of the interior of the intersection of the pair if an only if the closure of the union of every pair is a subset of the union of closures of the pair. (Contributed by RP, 19-Jun-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))

Theorem

ntrclsk13 44060*

The interior of the intersection of any pair is equal to the intersection of the interiors if and only if the closure of the unions of any pair is equal to the union of closures. (Contributed by RP, 19-Jun-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))

Theorem

ntrclsk4 44061*

Idempotence of the interior function is equivalent to idempotence of the closure function. (Contributed by RP, 10-Jul-2021.)

⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵(𝐼‘(𝐼‘𝑠)) = (𝐼‘𝑠) ↔ ∀𝑠 ∈ 𝒫 𝐵(𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠)))

Theorem

ntrneibex 44062*

If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then the base set exists. (Contributed by RP, 29-May-2021.)

⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → 𝐵 ∈ V)

Theorem

ntrneircomplex 44063*

The relative complement of the class 𝑆 exists as a subset of the base set. (Contributed by RP, 26-Jun-2021.)

⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵)

Theorem

ntrneif1o 44064*

If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, we may characterize the relation as part of a 1-to-1 onto function. (Contributed by RP, 29-May-2021.)

⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → 𝐹:(𝒫 𝐵 ↑_m 𝒫 𝐵)–1-1-onto→(𝒫 𝒫 𝐵 ↑_m 𝐵))

Theorem

ntrneiiex 44065*

If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then the interior function exists. (Contributed by RP, 29-May-2021.)

⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))

Theorem

ntrneinex 44066*

If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then the neighborhood function exists. (Contributed by RP, 29-May-2021.)

⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → 𝑁 ∈ (𝒫 𝒫 𝐵 ↑_m 𝐵))

Theorem

ntrneicnv 44067*

If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then converse of 𝐹 is known. (Contributed by RP, 29-May-2021.)

⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → ^◡𝐹 = (𝐵𝑂𝒫 𝐵))

Theorem

ntrneifv1 44068*

If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then the function value of 𝐹 is the neighborhood function. (Contributed by RP, 29-May-2021.)

⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (𝐹‘𝐼) = 𝑁)

Theorem

ntrneifv2 44069*

If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then the function value of converse of 𝐹 is the interior function. (Contributed by RP, 29-May-2021.)

⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (^◡𝐹‘𝑁) = 𝐼)

Theorem

ntrneiel 44070*

If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then there is an equivalence between membership in the interior of a set and non-membership in the closure of the complement of the set. (Contributed by RP, 29-May-2021.)

⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐼‘𝑆) ↔ 𝑆 ∈ (𝑁‘𝑋)))

Theorem

ntrneifv3 44071*

The value of the neighbors (convergents) expressed in terms of the interior (closure) function. (Contributed by RP, 26-Jun-2021.)

⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑁‘𝑋) = {𝑠 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ (𝐼‘𝑠)})

Theorem

ntrneineine0lem 44072*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (∃𝑠 ∈ 𝒫 𝐵𝑋 ∈ (𝐼‘𝑠) ↔ (𝑁‘𝑋) ≠ ∅))

Theorem

ntrneineine1lem 44073*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (∃𝑠 ∈ 𝒫 𝐵 ¬ 𝑋 ∈ (𝐼‘𝑠) ↔ (𝑁‘𝑋) ≠ 𝒫 𝐵))

Theorem

ntrneifv4 44074*

The value of the interior (closure) expressed in terms of the neighbors (convergents) function. (Contributed by RP, 26-Jun-2021.)

⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑆) = {𝑥 ∈ 𝐵 ∣ 𝑆 ∈ (𝑁‘𝑥)})

Theorem

ntrneiel2 44075*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐼‘(𝐼‘𝑆)) ↔ ∃𝑢 ∈ (𝑁‘𝑋)∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑆 ∈ (𝑁‘𝑦))))

Theorem

ntrneineine0 44076*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∃𝑠 ∈ 𝒫 𝐵𝑥 ∈ (𝐼‘𝑠) ↔ ∀𝑥 ∈ 𝐵 (𝑁‘𝑥) ≠ ∅))

Theorem

ntrneineine1 44077*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∃𝑠 ∈ 𝒫 𝐵 ¬ 𝑥 ∈ (𝐼‘𝑠) ↔ ∀𝑥 ∈ 𝐵 (𝑁‘𝑥) ≠ 𝒫 𝐵))

Theorem

ntrneicls00 44078*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → ((𝐼‘𝐵) = 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐵 ∈ (𝑁‘𝑥)))

Theorem

ntrneicls11 44079*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → ((𝐼‘∅) = ∅ ↔ ∀𝑥 ∈ 𝐵 ¬ ∅ ∈ (𝑁‘𝑥)))

Theorem

ntrneiiso 44080*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝑠 ⊆ 𝑡 → (𝐼‘𝑠) ⊆ (𝐼‘𝑡)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝑡) → 𝑡 ∈ (𝑁‘𝑥))))

Theorem

ntrneik2 44081*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵(𝐼‘𝑠) ⊆ 𝑠 ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) → 𝑥 ∈ 𝑠)))

Theorem

ntrneix2 44082*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑠 ⊆ (𝐼‘𝑠) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵(𝑥 ∈ 𝑠 → 𝑠 ∈ (𝑁‘𝑥))))

Theorem

ntrneikb 44083*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅)))

Theorem

ntrneixb 44084*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐼‘𝑠) ∪ (𝐼‘𝑡)) = 𝐵) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → (𝑠 ∈ (𝑁‘𝑥) ∨ 𝑡 ∈ (𝑁‘𝑥)))))

Theorem

ntrneik3 44085*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥))))

Theorem

ntrneix3 44086*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∪ 𝑡)) ⊆ ((𝐼‘𝑠) ∪ (𝐼‘𝑡)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) ∈ (𝑁‘𝑥) → (𝑠 ∈ (𝑁‘𝑥) ∨ 𝑡 ∈ (𝑁‘𝑥)))))

Theorem

ntrneik13 44087*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)))))

Theorem

ntrneix13 44088*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∪ 𝑡)) = ((𝐼‘𝑠) ∪ (𝐼‘𝑡)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∨ 𝑡 ∈ (𝑁‘𝑥)))))

Theorem

ntrneik4w 44089*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵(𝐼‘(𝐼‘𝑠)) = (𝐼‘𝑠) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) ↔ (𝐼‘𝑠) ∈ (𝑁‘𝑥))))

Theorem

ntrneik4 44090*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵(𝐼‘(𝐼‘𝑠)) = (𝐼‘𝑠) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) ↔ ∃𝑢 ∈ (𝑁‘𝑥)∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑠 ∈ (𝑁‘𝑦)))))

Theorem

clsneibex 44091

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)

Theorem

clsneircomplex 44092

The relative complement of the class 𝑆 exists as a subset of the base set. (Contributed by RP, 26-Jun-2021.)

⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    ⇒   ⊢ (𝜑 → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵)

Theorem

clsneif1o 44093*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑_m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    ⇒   ⊢ (𝜑 → 𝐻:(𝒫 𝐵 ↑_m 𝒫 𝐵)–1-1-onto→(𝒫 𝒫 𝐵 ↑_m 𝐵))

Theorem

clsneicnv 44094*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑_m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    ⇒   ⊢ (𝜑 → ^◡𝐻 = (𝐷 ∘ (𝐵𝑂𝒫 𝐵)))

Theorem

clsneikex 44095*

If closure and neighborhoods functions are related, the closure function exists. (Contributed by RP, 27-Jun-2021.)

⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑_m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))

Theorem

clsneinex 44096*

If closure and neighborhoods functions are related, the neighborhoods function exists. (Contributed by RP, 27-Jun-2021.)

⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑_m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    ⇒   ⊢ (𝜑 → 𝑁 ∈ (𝒫 𝒫 𝐵 ↑_m 𝐵))

Theorem

clsneiel1 44097*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑_m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐾‘𝑆) ↔ ¬ (𝐵 ∖ 𝑆) ∈ (𝑁‘𝑋)))

Theorem

clsneiel2 44098*

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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑_m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐾‘(𝐵 ∖ 𝑆)) ↔ ¬ 𝑆 ∈ (𝑁‘𝑋)))

Theorem

clsneifv3 44099*

Value of the neighborhoods (convergents) in terms of the closure (interior) function. (Contributed by RP, 27-Jun-2021.)

⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑_m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑁‘𝑋) = {𝑠 ∈ 𝒫 𝐵 ∣ ¬ 𝑋 ∈ (𝐾‘(𝐵 ∖ 𝑠))})

Theorem

clsneifv4 44100*

Value of the closure (interior) function in terms of the neighborhoods (convergents) function. (Contributed by RP, 27-Jun-2021.)

⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑_m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑_m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝐾‘𝑆) = {𝑥 ∈ 𝐵 ∣ ¬ (𝐵 ∖ 𝑆) ∈ (𝑁‘𝑥)})