![]() |
Metamath
Proof Explorer Theorem List (p. 432 of 480) | < 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: | ![]() (1-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | isotone1 43101* | Two different ways to say subset relation persists across applications of a function. (Contributed by RP, 31-May-2021.) |
⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏))) | ||
Theorem | isotone2 43102* | Two different ways to say subset relation persists across applications of a function. (Contributed by RP, 31-May-2021.) |
⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝐹‘(𝑎 ∩ 𝑏)) ⊆ ((𝐹‘𝑎) ∩ (𝐹‘𝑏))) | ||
Theorem | ntrk1k3eqk13 43103* | 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 43104* | 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 43105* | 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 43106* | 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 43107* | 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 43108* | 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 43109* | 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 43110* | 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 43111* | 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 43112* | The value of the interior (closure) expressed in terms of the closure (interior). (Contributed by RP, 25-Jun-2021.) |
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗)))))) & ⊢ 𝐷 = (𝑂‘𝐵) & ⊢ (𝜑 → 𝐼𝐷𝐾) & ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵) ⇒ ⊢ (𝜑 → (𝐼‘𝑆) = (𝐵 ∖ (𝐾‘(𝐵 ∖ 𝑆)))) | ||
Theorem | ntrclsfveq1 43113* | If interior and closure functions are related then specific function values are complementary. (Contributed by RP, 27-Jun-2021.) |
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗)))))) & ⊢ 𝐷 = (𝑂‘𝐵) & ⊢ (𝜑 → 𝐼𝐷𝐾) & ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝒫 𝐵) ⇒ ⊢ (𝜑 → ((𝐼‘𝑆) = 𝐶 ↔ (𝐾‘(𝐵 ∖ 𝑆)) = (𝐵 ∖ 𝐶))) | ||
Theorem | ntrclsfveq2 43114* | If interior and closure functions are related then specific function values are complementary. (Contributed by RP, 27-Jun-2021.) |
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗)))))) & ⊢ 𝐷 = (𝑂‘𝐵) & ⊢ (𝜑 → 𝐼𝐷𝐾) & ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝒫 𝐵) ⇒ ⊢ (𝜑 → ((𝐼‘(𝐵 ∖ 𝑆)) = 𝐶 ↔ (𝐾‘𝑆) = (𝐵 ∖ 𝐶))) | ||
Theorem | ntrclsfveq 43115* | 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 43116* | 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 43117* | 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 43118* | 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 43119* | 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 43120* | 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 43121* | An interior function is contracting if and only if the closure function is expansive. (Contributed by RP, 9-Jun-2021.) |
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗)))))) & ⊢ 𝐷 = (𝑂‘𝐵) & ⊢ (𝜑 → 𝐼𝐷𝐾) ⇒ ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵(𝐼‘𝑠) ⊆ 𝑠 ↔ ∀𝑠 ∈ 𝒫 𝐵𝑠 ⊆ (𝐾‘𝑠))) | ||
Theorem | ntrclskb 43122* | 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 43123* | 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 43124* | 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 43125* | Idempotence of the interior function is equivalent to idempotence of the closure function. (Contributed by RP, 10-Jul-2021.) |
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗)))))) & ⊢ 𝐷 = (𝑂‘𝐵) & ⊢ (𝜑 → 𝐼𝐷𝐾) ⇒ ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵(𝐼‘(𝐼‘𝑠)) = (𝐼‘𝑠) ↔ ∀𝑠 ∈ 𝒫 𝐵(𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠))) | ||
Theorem | ntrneibex 43126* | 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 43127* | 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 43128* | 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 43129* | 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 43130* | 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 43131* | 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 43132* | 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 43133* | 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 43134* | 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 43135* | 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 43136* | 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 43137* | 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 43138* | 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 43139* | 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 43140* | 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 43141* | 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 43142* | 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 43143* | 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 43144* | 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 43145* | 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 43146* | 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 43147* | 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 43148* | 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 43149* | 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 43150* | 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 43151* | 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 43152* | 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 43153* | 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 43154* | 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 43155 | 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 43156 | The relative complement of the class 𝑆 exists as a subset of the base set. (Contributed by RP, 26-Jun-2021.) |
⊢ 𝐷 = (𝑃‘𝐵) & ⊢ 𝐻 = (𝐹 ∘ 𝐷) & ⊢ (𝜑 → 𝐾𝐻𝑁) ⇒ ⊢ (𝜑 → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵) | ||
Theorem | clsneif1o 43157* | 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 43158* | 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 43159* | 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 43160* | 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 43161* | 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 43162* | 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 43163* | 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 43164* | Value of the closure (interior) function in terms of the neighborhoods (convergents) function. (Contributed by RP, 27-Jun-2021.) |
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)}))) & ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜)))))) & ⊢ 𝐷 = (𝑃‘𝐵) & ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵) & ⊢ 𝐻 = (𝐹 ∘ 𝐷) & ⊢ (𝜑 → 𝐾𝐻𝑁) & ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵) ⇒ ⊢ (𝜑 → (𝐾‘𝑆) = {𝑥 ∈ 𝐵 ∣ ¬ (𝐵 ∖ 𝑆) ∈ (𝑁‘𝑥)}) | ||
Theorem | neicvgbex 43165 | 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) | ||
Theorem | neicvgrcomplex 43166 | The relative complement of the class 𝑆 exists as a subset of the base set. (Contributed by RP, 26-Jun-2021.) |
⊢ 𝐷 = (𝑃‘𝐵) & ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺)) & ⊢ (𝜑 → 𝑁𝐻𝑀) ⇒ ⊢ (𝜑 → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵) | ||
Theorem | neicvgf1o 43167* | 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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)}))) & ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜)))))) & ⊢ 𝐷 = (𝑃‘𝐵) & ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵) & ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵) & ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺)) & ⊢ (𝜑 → 𝑁𝐻𝑀) ⇒ ⊢ (𝜑 → 𝐻:(𝒫 𝒫 𝐵 ↑m 𝐵)–1-1-onto→(𝒫 𝒫 𝐵 ↑m 𝐵)) | ||
Theorem | neicvgnvo 43168* | If neighborhood and convergent functions are related by operator 𝐻, it is its own converse function. (Contributed by RP, 11-Jun-2021.) |
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)}))) & ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜)))))) & ⊢ 𝐷 = (𝑃‘𝐵) & ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵) & ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵) & ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺)) & ⊢ (𝜑 → 𝑁𝐻𝑀) ⇒ ⊢ (𝜑 → ◡𝐻 = 𝐻) | ||
Theorem | neicvgnvor 43169* | If neighborhood and convergent functions are related by operator 𝐻, the relationship holds with the functions swapped. (Contributed by RP, 11-Jun-2021.) |
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)}))) & ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜)))))) & ⊢ 𝐷 = (𝑃‘𝐵) & ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵) & ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵) & ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺)) & ⊢ (𝜑 → 𝑁𝐻𝑀) ⇒ ⊢ (𝜑 → 𝑀𝐻𝑁) | ||
Theorem | neicvgmex 43170* | If the neighborhoods and convergents functions are related, the convergents function exists. (Contributed by RP, 27-Jun-2021.) |
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)}))) & ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜)))))) & ⊢ 𝐷 = (𝑃‘𝐵) & ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵) & ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵) & ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺)) & ⊢ (𝜑 → 𝑁𝐻𝑀) ⇒ ⊢ (𝜑 → 𝑀 ∈ (𝒫 𝒫 𝐵 ↑m 𝐵)) | ||
Theorem | neicvgnex 43171* | If the neighborhoods and convergents functions are related, the neighborhoods function exists. (Contributed by RP, 27-Jun-2021.) |
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)}))) & ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜)))))) & ⊢ 𝐷 = (𝑃‘𝐵) & ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵) & ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵) & ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺)) & ⊢ (𝜑 → 𝑁𝐻𝑀) ⇒ ⊢ (𝜑 → 𝑁 ∈ (𝒫 𝒫 𝐵 ↑m 𝐵)) | ||
Theorem | neicvgel1 43172* | 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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)}))) & ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜)))))) & ⊢ 𝐷 = (𝑃‘𝐵) & ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵) & ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵) & ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺)) & ⊢ (𝜑 → 𝑁𝐻𝑀) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵) ⇒ ⊢ (𝜑 → (𝑆 ∈ (𝑁‘𝑋) ↔ ¬ (𝐵 ∖ 𝑆) ∈ (𝑀‘𝑋))) | ||
Theorem | neicvgel2 43173* | 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 ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)}))) & ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜)))))) & ⊢ 𝐷 = (𝑃‘𝐵) & ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵) & ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵) & ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺)) & ⊢ (𝜑 → 𝑁𝐻𝑀) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵) ⇒ ⊢ (𝜑 → ((𝐵 ∖ 𝑆) ∈ (𝑁‘𝑋) ↔ ¬ 𝑆 ∈ (𝑀‘𝑋))) | ||
Theorem | neicvgfv 43174* | The value of the neighborhoods (convergents) in terms of the convergents (neighborhoods) function. (Contributed by RP, 27-Jun-2021.) |
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)}))) & ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜)))))) & ⊢ 𝐷 = (𝑃‘𝐵) & ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵) & ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵) & ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺)) & ⊢ (𝜑 → 𝑁𝐻𝑀) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑁‘𝑋) = {𝑠 ∈ 𝒫 𝐵 ∣ ¬ (𝐵 ∖ 𝑠) ∈ (𝑀‘𝑋)}) | ||
Theorem | ntrrn 43175 | 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 𝐼 ⊆ 𝐽) | ||
Theorem | ntrf 43176 | 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 → 𝐼:𝒫 𝑋⟶𝐽) | ||
Theorem | ntrf2 43177 | The interior function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐼 = (int‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐼:𝒫 𝑋⟶𝒫 𝑋) | ||
Theorem | ntrelmap 43178 | The interior function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐼 = (int‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐼 ∈ (𝒫 𝑋 ↑m 𝒫 𝑋)) | ||
Theorem | clsf2 43179 | The closure function is a map from the powerset of the base set to itself. This is less precise than clsf 22772. (Contributed by RP, 22-Apr-2021.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐾:𝒫 𝑋⟶𝒫 𝑋) | ||
Theorem | clselmap 43180 | The closure function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐾 ∈ (𝒫 𝑋 ↑m 𝒫 𝑋)) | ||
Theorem | dssmapntrcls 43181* | The interior and closure operators on a topology are duals of each other. See also kur14lem2 34496. (Contributed by RP, 21-Apr-2021.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) & ⊢ 𝐼 = (int‘𝐽) & ⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))))) & ⊢ 𝐷 = (𝑂‘𝑋) ⇒ ⊢ (𝐽 ∈ Top → 𝐼 = (𝐷‘𝐾)) | ||
Theorem | dssmapclsntr 43182* | The closure and interior operators on a topology are duals of each other. See also kur14lem2 34496. (Contributed by RP, 22-Apr-2021.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) & ⊢ 𝐼 = (int‘𝐽) & ⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))))) & ⊢ 𝐷 = (𝑂‘𝑋) ⇒ ⊢ (𝐽 ∈ Top → 𝐾 = (𝐷‘𝐼)) | ||
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 22722 is an example of a topology with an empty base set. This divergence is unlikely to pose serious problems. | ||
Theorem | gneispa 43183* | 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‘𝐽)‘{𝑝})𝑝 ∈ 𝑛)) | ||
Theorem | gneispb 43184* | 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‘𝐽)‘{𝑃}))) | ||
Theorem | gneispace2 43185* | 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 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))) | ||
Theorem | gneispace3 43186* | 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 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))) | ||
Theorem | gneispace 43187* | 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 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))))) | ||
Theorem | gneispacef 43188* | 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 𝐹 ∖ {∅}) ∖ {∅})) | ||
Theorem | gneispacef2 43189* | 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 𝐹) | ||
Theorem | gneispacefun 43190* | A generic neighborhood space is a function. (Contributed by RP, 15-Apr-2021.) |
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))} ⇒ ⊢ (𝐹 ∈ 𝐴 → Fun 𝐹) | ||
Theorem | gneispacern 43191* | 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 𝐹 ∖ {∅}) ∖ {∅})) | ||
Theorem | gneispacern2 43192* | 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 𝐹) | ||
Theorem | gneispace0nelrn 43193* | A generic neighborhood space has a nonempty set of neighborhoods for every point in its domain. (Contributed by RP, 15-Apr-2021.) |
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))} ⇒ ⊢ (𝐹 ∈ 𝐴 → ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅) | ||
Theorem | gneispace0nelrn2 43194* | A generic neighborhood space has a nonempty set of neighborhoods for every point in its domain. (Contributed by RP, 15-Apr-2021.) |
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))} ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑃 ∈ dom 𝐹) → (𝐹‘𝑃) ≠ ∅) | ||
Theorem | gneispace0nelrn3 43195* | A generic neighborhood space has a nonempty set of neighborhoods for every point in its domain. (Contributed by RP, 15-Apr-2021.) |
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))} ⇒ ⊢ (𝐹 ∈ 𝐴 → ¬ ∅ ∈ ran 𝐹) | ||
Theorem | gneispaceel 43196* | Every neighborhood of a point in a generic neighborhood space contains that point. (Contributed by RP, 15-Apr-2021.) |
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))} ⇒ ⊢ (𝐹 ∈ 𝐴 → ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)𝑝 ∈ 𝑛) | ||
Theorem | gneispaceel2 43197* | Every neighborhood of a point in a generic neighborhood space contains that point. (Contributed by RP, 15-Apr-2021.) |
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))} ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑃 ∈ dom 𝐹 ∧ 𝑁 ∈ (𝐹‘𝑃)) → 𝑃 ∈ 𝑁) | ||
Theorem | gneispacess 43198* | 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 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))) | ||
Theorem | gneispacess2 43199* | 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 𝐹 ∧ 𝑁 ⊆ 𝑆)) → 𝑆 ∈ (𝐹‘𝑃)) | ||
See https://kerodon.net/ for a work in progress by Jacob Lurie. | ||
See https://kerodon.net/tag/0004 for introduction to the topological simplex of dimension 𝑁. | ||
Theorem | k0004lem1 43200 | Application of ssin 4229 to range of a function. (Contributed by RP, 1-Apr-2021.) |
⊢ (𝐷 = (𝐵 ∩ 𝐶) → ((𝐹:𝐴⟶𝐵 ∧ (𝐹 “ 𝐴) ⊆ 𝐶) ↔ 𝐹:𝐴⟶𝐷)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |