P. 416 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

rfovcnvf1od 41501*

Properties of the operator, (𝐴𝑂𝐵), which maps between relations and functions for relations between base sets, 𝐴 and 𝐵. (Contributed by RP, 27-Apr-2021.)

⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥 ∈ 𝑎 ↦ {𝑦 ∈ 𝑏 ∣ 𝑥𝑟𝑦})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐹 = (𝐴𝑂𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝒫 (𝐴 × 𝐵)–1-1-onto→(𝒫 𝐵 ↑_m 𝐴) ∧ ^◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})))

Theorem

rfovcnvd 41502*

Value of the converse of the operator, (𝐴𝑂𝐵), which maps between relations and functions for relations between base sets, 𝐴 and 𝐵. (Contributed by RP, 27-Apr-2021.)

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

Theorem

rfovf1od 41503*

The value of the operator, (𝐴𝑂𝐵), which maps between relations and functions for relations between base sets, 𝐴 and 𝐵, is a bijection. (Contributed by RP, 27-Apr-2021.)

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

Theorem

rfovcnvfvd 41504*

Value of the converse of the operator, (𝐴𝑂𝐵), which maps between relations and functions for relations between base sets, 𝐴 and 𝐵, evaluated at function 𝐺. (Contributed by RP, 27-Apr-2021.)

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

Theorem

fsovd 41505*

Value of 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 𝐵. (Contributed by RP, 25-Apr-2021.)

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

Theorem

fsovrfovd 41506*

The operator which gives a 1-to-1 a mapping to a subset and a reverse mapping from elements can be composed from the operator which gives a 1-to-1 mapping between relations and functions to subsets and the converse operator. (Contributed by RP, 15-May-2021.)

⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝑅 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑢 ∈ 𝑎 ↦ {𝑣 ∈ 𝑏 ∣ 𝑢𝑟𝑣})))    &   ⊢ 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ^◡𝑠))    ⇒   ⊢ (𝜑 → (𝐴𝑂𝐵) = ((𝐵𝑅𝐴) ∘ ((𝐴𝐶𝐵) ∘ ^◡(𝐴𝑅𝐵))))

Theorem

fsovfvd 41507*

Value of 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 𝐵, when applied to function 𝐹. (Contributed by RP, 25-Apr-2021.)

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

Theorem

fsovfvfvd 41508*

Value of 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 𝐵, when applied to function 𝐹 and element 𝑌. (Contributed by RP, 25-Apr-2021.)

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

Theorem

fsovfd 41509*

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 41510*

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 41511*

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 41512*

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 41513*

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 41514*

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 41515*

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 41516*

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 41517*

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 41518*

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 41519*

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 𝒫 𝐵)))

20.31.4.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 41514. 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 41556, ntrneiel 41580, neicvgel1 41618
	¬ (𝐵 ∖ 𝑆) ∈ (𝑁‘𝑋)	↔	¬ 𝑋 ∈ (𝐼‘(𝐵 ∖ 𝑆))	↔	𝑋 ∈ (𝐾‘𝑆)	↔	𝑆 ∈ (𝑀‘𝑋)
Neighborhoods	(𝑁‘𝑋)	=	{𝑠 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ (𝐼‘𝑠)}	=	{𝑠 ∈ 𝒫 𝐵 ∣ ¬ 𝑋 ∈ (𝐾‘(𝐵 ∖ 𝑠))}	=	{𝑠 ∈ 𝒫 𝐵 ∣ ¬ (𝐵 ∖ 𝑠) ∈ (𝑀‘𝑋)}	ntrneifv3 41581, clsneifv3 41609, neicvgfv 41620
Interior	{𝑥 ∈ 𝐵 ∣ 𝑆 ∈ (𝑁‘𝑥)}	=	(𝐼‘𝑆)	=	(𝐵 ∖ (𝐾‘(𝐵 ∖ 𝑆)))	=	{𝑥 ∈ 𝐵 ∣ ¬ (𝐵 ∖ 𝑆) ∈ (𝑀‘𝑥)}	ntrneifv4 41584, ntrclsfv 41558, clsneifv4 41610
Closure	{𝑥 ∈ 𝐵 ∣ ¬ (𝐵 ∖ 𝑆) ∈ (𝑁‘𝑥)}	=	(𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑆)))	=	(𝐾‘𝑆)	=	{𝑥 ∈ 𝐵 ∣ 𝑆 ∈ (𝑀‘𝑥)}	clsneifv4 41610, ntrclsfv 41558, ntrneifv4 41584
Convergents	{𝑠 ∈ 𝒫 𝐵 ∣ ¬ (𝐵 ∖ 𝑠) ∈ (𝑁‘𝑋)}	=	{𝑠 ∈ 𝒫 𝐵 ∣ ¬ 𝑋 ∈ (𝐼‘(𝐵 ∖ 𝑠))}	=	{𝑠 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ (𝐾‘𝑠)}	=	(𝑀‘𝑋)	neicvgfv 41620, clsneifv3 41609, ntrneifv3 41581

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 41564, ntrneineine0 41586, ntrneineine1 41587
KA' No neighborhood is equal to the full powerset.	(𝑁‘𝑥) ≠ 𝒫 𝐵	∃𝑢 ∈ 𝒫 𝐵¬ 𝑥 ∈ (𝐼‘𝑢)	∃𝑢 ∈ 𝒫 𝐵𝑥 ∈ (𝐾‘𝑢)	(𝑀‘𝑥) ≠ ∅	ntrclsneine0 41564, ntrneineine0 41586, ntrneineine1 41587
K0 Preservation of the Nullary Union of Closures	𝐵 ∈ (𝑁‘𝑥)	(𝐼‘𝐵) = 𝐵	(𝐾‘∅) = ∅	¬ ∅ ∈ (𝑀‘𝑥)	ntrclscls00 41565, ntrneicls00 41588, ntrneicls11 41589
KA Preservation of the Nullary Union of Interiors	¬ ∅ ∈ (𝑁‘𝑥)	(𝐼‘∅) = ∅	(𝐾‘𝐵) = 𝐵	𝐵 ∈ (𝑀‘𝑥)	ntrclscls00 41565, ntrneicls00 41588, ntrneicls11 41589
K1 Isotonic Montonic	((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝑡) → 𝑡 ∈ (𝑁‘𝑥))	(𝑠 ⊆ 𝑡 → (𝐼‘𝑠) ⊆ (𝐼‘𝑡)) — or — ((𝐼‘𝑠) ∪ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∪ 𝑡)) — or — (𝐼‘(𝑠 ∩ 𝑡)) ⊆ ((𝐼‘𝑠) ∩ (𝐼‘𝑡))	(𝑠 ⊆ 𝑡 → (𝐾‘𝑠) ⊆ (𝐾‘𝑡)) — or — ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) ⊆ (𝐾‘(𝑠 ∪ 𝑡)) — or — (𝐾‘(𝑠 ∩ 𝑡)) ⊆ ((𝐾‘𝑠) ∩ (𝐾‘𝑡))	((𝑠 ∈ (𝑀‘𝑥) ∧ 𝑠 ⊆ 𝑡) → 𝑡 ∈ (𝑀‘𝑥))	isotone1 41547, isotone2 41548, ntrclsiso 41566, ntrneiiso 41590
K2 Closure is Expansive	(𝑠 ∈ (𝑁‘𝑥) → 𝑥 ∈ 𝑠)	(𝐼‘𝑠) ⊆ 𝑠	𝑠 ⊆ (𝐾‘𝑠)	(𝑥 ∈ 𝑠 → 𝑠 ∈ (𝑀‘𝑥))	ntrclsk2 41567, ntrneik2 41591, ntrneix2 41592
KB Non-disjoint Neighborhoods	((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅)	((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅)	((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)	((𝑠 ∪ 𝑡) = 𝐵 → (𝑠 ∈ (𝑀‘𝑥) ∨ 𝑡 ∈ (𝑀‘𝑥)))	ntrclskb 41568, ntrneikb 41593, ntrneixb 41594
K3 Closure is Sub-linear	((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥))	((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡))	(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))	((𝑠 ∪ 𝑡) ∈ (𝑀‘𝑥) → (𝑠 ∈ (𝑀‘𝑥) ∨ 𝑡 ∈ (𝑀‘𝑥)))	ntrclsk3 41569, ntrneik3 41595, ntrneix3 41596
K13 Closure is finitely linear	((𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)))	(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡))	(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))	((𝑠 ∪ 𝑡) ∈ (𝑀‘𝑥) ↔ (𝑠 ∈ (𝑀‘𝑥) ∨ 𝑡 ∈ (𝑀‘𝑥)))	ntrclsk13 41570, ntrneik13 41597, ntrneix13 41598
K4 Closure is idempotent	(𝑠 ∈ (𝑁‘𝑥) ↔ ∃𝑢 ∈ (𝑁‘𝑥)∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑠 ∈ (𝑁‘𝑦)))	(𝐼‘(𝐼‘𝑠)) = (𝐼‘𝑠)	(𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠)	(𝑠 ∈ (𝑀‘𝑥) ↔ ∃𝑢 ∈ (𝑀‘𝑥)∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑠 ∈ (𝑀‘𝑦)))	ntrclsk4 41571, ntrneik4 41600

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 41536, ntrkbimka 41537, neik0imk0p 41535
Min Strong Generalized Neighborhood Space	K2, K3	KA', KA, KB	ntrk2imkb 41536, ntrkbimka 41537, neik0imk0p 41535
Gniłka Extended Topology	K0', K1	K0	neik0pk1imk0 41546
Brissaud Space	K0, K2	K0', KA', KA, KB	neik0imk0p 41535, ntrk2imkb 41536, ntrkbimka 41537
Neighborhood Space	K0', K1, K2	K0, KA', KA, KB	neik0pk1imk0 41546, ntrk2imkb 41536, ntrkbimka 41537, neik0imk0p 41535
Davey and Priestley Intersection Structure	K1, K4
Moore Closure Space	K1, K2, K4	KA', KA, KB	ntrk2imkb 41536, ntrkbimka 41537, neik0imk0p 41535
Convex Closure Space	K0', K1, K2, K4	K0, KA', KA, KB	neik0pk1imk0 41546, ntrk2imkb 41536, ntrkbimka 41537, neik0imk0p 41535
Smyth Neighborhood Space	K0', K13	K0, K1, K3	neik0pk1imk0 41546, ntrk1k3eqk13 41549
Čech Closure Space Pretopological Space	K0', K2, K13	K0, K1, KA', KA, KB, K3	neik0pk1imk0 41546, ntrk2imkb 41536, ntrkbimka 41537, neik0imk0p 41535, ntrk1k3eqk13 41549
Topological Space	K0', K2, K13, K4	K0, K1, KA', KA, KB, K3	neik0pk1imk0 41546, ntrk2imkb 41536, ntrkbimka 41537, neik0imk0p 41535, ntrk1k3eqk13 41549
Alexandroff Space	K0', K2, K5	K0, K1, KA', KA, KB, K3, K13	neik0pk1imk0 41546, ntrk2imkb 41536, ntrkbimka 41537, neik0imk0p 41535, ntrk1k3eqk13 41549, TBD
Alexandroff Topological Space	K0', K2, K4, K5	K0, K1, KA', KA, KB, K3, K13	neik0pk1imk0 41546, ntrk2imkb 41536, ntrkbimka 41537, neik0imk0p 41535, ntrk1k3eqk13 41549, TBD

Theorem

or3or 41520

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

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

Theorem

andi3or 41521

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

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

Theorem

uneqsn 41522

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

df3o2 41523

Ordinal 3 is the unordered triple containing ordinals 0, 1, and 2. (Contributed by RP, 8-Jul-2021.)

⊢ 3_o = {∅, 1_o, 2_o}

Theorem

df3o3 41524

Ordinal 3, fully expanded. (Contributed by RP, 8-Jul-2021.)

⊢ 3_o = {∅, {∅}, {∅, {∅}}}

Theorem

brfvimex 41525

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 41526*

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 41527*

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 41528*

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 41529

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

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

Theorem

brcofffn 41530

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

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

Theorem

brco2f1o 41531

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

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

Theorem

brco3f1o 41532

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 41533

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 41534

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

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

Theorem

neik0imk0p 41535

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 41536*

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 41537*

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 41538*

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 41537. (Contributed by RP, 12-Jun-2021.)

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

Theorem

clsk3nimkb 41539*

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 41540

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 41541*

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 41542*

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 41543*

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 41544*

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 41545*

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 41546*

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

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

Theorem

isotone1 41547*

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

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

Theorem

isotone2 41548*

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

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

Theorem

ntrk1k3eqk13 41549*

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 41550*

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 41551*

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 41552*

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 41553*

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 41554*

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 41555*

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 41556*

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 41557*

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 41558*

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

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

Theorem

ntrclsfveq1 41559*

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

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

Theorem

ntrclsfveq2 41560*

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

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

Theorem

ntrclsfveq 41561*

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 41562*

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 41563*

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 41564*

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 41565*

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 41566*

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 41567*

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

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

Theorem

ntrclskb 41568*

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 41569*

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 41570*

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 41571*

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

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

Theorem

ntrneibex 41572*

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 41573*

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 41574*

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 41575*

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 41576*

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 41577*

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 41578*

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 41579*

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 41580*

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 41581*

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 41582*

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 41583*

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 41584*

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 41585*

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 41586*

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 41587*

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 41588*

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 41589*

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 41590*

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 41591*

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 41592*

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 41593*

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 41594*

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 41595*

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 41596*

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 41597*

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 41598*

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 41599*

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 41600*

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