![]() |
Metamath
Proof Explorer Theorem List (p. 436 of 483) | < 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-30722) |
![]() (30723-32245) |
![]() (32246-48229) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ntrneifv2 43501* | 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 43502* | 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 43503* | 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 43504* | 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 43505* | 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 43506* | 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 43507* | 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 43508* | 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 43509* | 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 43510* | 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 43511* | 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 43512* | 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 43513* | 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 43514* | 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 43515* | 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 43516* | 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 43517* | 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 43518* | 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 43519* | 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 43520* | 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 43521* | 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 43522* | 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 43523 | 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 43524 | The relative complement of the class 𝑆 exists as a subset of the base set. (Contributed by RP, 26-Jun-2021.) |
⊢ 𝐷 = (𝑃‘𝐵) & ⊢ 𝐻 = (𝐹 ∘ 𝐷) & ⊢ (𝜑 → 𝐾𝐻𝑁) ⇒ ⊢ (𝜑 → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵) | ||
Theorem | clsneif1o 43525* | 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 43526* | 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 43527* | 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 43528* | 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 43529* | 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 43530* | 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 43531* | 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 43532* | 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 43533 | 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 43534 | The relative complement of the class 𝑆 exists as a subset of the base set. (Contributed by RP, 26-Jun-2021.) |
⊢ 𝐷 = (𝑃‘𝐵) & ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺)) & ⊢ (𝜑 → 𝑁𝐻𝑀) ⇒ ⊢ (𝜑 → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵) | ||
Theorem | neicvgf1o 43535* | 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 43536* | 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 43537* | 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 43538* | 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 43539* | 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 43540* | 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 43541* | 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 43542* | 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 43543 | 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 43544 | 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 43545 | 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 43546 | 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 43547 | The closure function is a map from the powerset of the base set to itself. This is less precise than clsf 22946. (Contributed by RP, 22-Apr-2021.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐾:𝒫 𝑋⟶𝒫 𝑋) | ||
Theorem | clselmap 43548 | 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 43549* | The interior and closure operators on a topology are duals of each other. See also kur14lem2 34812. (Contributed by RP, 21-Apr-2021.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) & ⊢ 𝐼 = (int‘𝐽) & ⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))))) & ⊢ 𝐷 = (𝑂‘𝑋) ⇒ ⊢ (𝐽 ∈ Top → 𝐼 = (𝐷‘𝐾)) | ||
Theorem | dssmapclsntr 43550* | The closure and interior operators on a topology are duals of each other. See also kur14lem2 34812. (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 22896 is an example of a topology with an empty base set. This divergence is unlikely to pose serious problems. | ||
Theorem | gneispa 43551* | 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 43552* | 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 43553* | 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 43554* | 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 43555* | 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 43556* | 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 43557* | 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 43558* | A generic neighborhood space is a function. (Contributed by RP, 15-Apr-2021.) |
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))} ⇒ ⊢ (𝐹 ∈ 𝐴 → Fun 𝐹) | ||
Theorem | gneispacern 43559* | 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 43560* | 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 43561* | 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 43562* | 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 43563* | 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 43564* | 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 43565* | 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 43566* | 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 43567* | 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 43568 | Application of ssin 4227 to range of a function. (Contributed by RP, 1-Apr-2021.) |
⊢ (𝐷 = (𝐵 ∩ 𝐶) → ((𝐹:𝐴⟶𝐵 ∧ (𝐹 “ 𝐴) ⊆ 𝐶) ↔ 𝐹:𝐴⟶𝐷)) | ||
Theorem | k0004lem2 43569 | A mapping with a particular restricted range is also a mapping to that range. (Contributed by RP, 1-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝐵) → ((𝐹 ∈ (𝐵 ↑m 𝐴) ∧ (𝐹 “ 𝐴) ⊆ 𝐶) ↔ 𝐹 ∈ (𝐶 ↑m 𝐴))) | ||
Theorem | k0004lem3 43570 | When the value of a mapping on a singleton is known, the mapping is a completely known singleton. (Contributed by RP, 2-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∈ (𝐵 ↑m {𝐴}) ∧ (𝐹‘𝐴) = 𝐶) ↔ 𝐹 = {〈𝐴, 𝐶〉})) | ||
Theorem | k0004val 43571* | The topological simplex of dimension 𝑁 is the set of real vectors where the components are nonnegative and sum to 1. (Contributed by RP, 29-Mar-2021.) |
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑m (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡‘𝑘) = 1}) ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝐴‘𝑁) = {𝑡 ∈ ((0[,]1) ↑m (1...(𝑁 + 1))) ∣ Σ𝑘 ∈ (1...(𝑁 + 1))(𝑡‘𝑘) = 1}) | ||
Theorem | k0004ss1 43572* | The topological simplex of dimension 𝑁 is a subset of the real vectors of dimension (𝑁 + 1). (Contributed by RP, 29-Mar-2021.) |
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑m (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡‘𝑘) = 1}) ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝐴‘𝑁) ⊆ (ℝ ↑m (1...(𝑁 + 1)))) | ||
Theorem | k0004ss2 43573* | The topological simplex of dimension 𝑁 is a subset of the base set of a real vector space of dimension (𝑁 + 1). (Contributed by RP, 29-Mar-2021.) |
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑m (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡‘𝑘) = 1}) ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝐴‘𝑁) ⊆ (Base‘(ℝ^‘(1...(𝑁 + 1))))) | ||
Theorem | k0004ss3 43574* | The topological simplex of dimension 𝑁 is a subset of the base set of Euclidean space of dimension (𝑁 + 1). (Contributed by RP, 29-Mar-2021.) |
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑m (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡‘𝑘) = 1}) ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝐴‘𝑁) ⊆ (Base‘(𝔼hil‘(𝑁 + 1)))) | ||
Theorem | k0004val0 43575* | The topological simplex of dimension 0 is a singleton. (Contributed by RP, 2-Apr-2021.) |
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑m (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡‘𝑘) = 1}) ⇒ ⊢ (𝐴‘0) = {{〈1, 1〉}} | ||
Theorem | inductionexd 43576 | Simple induction example. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝑁 ∈ ℕ → 3 ∥ ((4↑𝑁) + 5)) | ||
Theorem | wwlemuld 43577 | Natural deduction form of lemul2d 13087. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵)) & ⊢ (𝜑 → 0 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
Theorem | leeq1d 43578 | Specialization of breq1d 5153 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐵 ≤ 𝐶) | ||
Theorem | leeq2d 43579 | Specialization of breq2d 5155 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐶 = 𝐷) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐷) | ||
Theorem | absmulrposd 43580 | Specialization of absmuld with absidd 15396. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 · 𝐵)) = (𝐴 · (abs‘𝐵))) | ||
Theorem | imadisjld 43581 | Natural dduction form of one side of imadisj 6078. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → (dom 𝐴 ∩ 𝐵) = ∅) ⇒ ⊢ (𝜑 → (𝐴 “ 𝐵) = ∅) | ||
Theorem | wnefimgd 43582 | The image of a mapping from A is nonempty if A is nonempty. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (𝐹 “ 𝐴) ≠ ∅) | ||
Theorem | fco2d 43583 | Natural deduction form of fco2 6745. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐴⟶𝐶) | ||
Theorem | wfximgfd 43584 | The value of a function on its domain is in the image of the function. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (𝐹‘𝐶) ∈ (𝐹 “ 𝐴)) | ||
Theorem | extoimad 43585* | If |f(x)| <= C for all x then it applies to all x in the image of |f(x)| (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 𝐶) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ (abs “ (𝐹 “ ℝ))𝑥 ≤ 𝐶) | ||
Theorem | imo72b2lem0 43586* | Lemma for imo72b2 43593. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐺:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘(𝐴 + 𝐵)) + (𝐹‘(𝐴 − 𝐵))) = (2 · ((𝐹‘𝐴) · (𝐺‘𝐵)))) & ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1) ⇒ ⊢ (𝜑 → ((abs‘(𝐹‘𝐴)) · (abs‘(𝐺‘𝐵))) ≤ sup((abs “ (𝐹 “ ℝ)), ℝ, < )) | ||
Theorem | suprleubrd 43587* | Natural deduction form of specialized suprleub 12205. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝐵) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ, < ) ≤ 𝐵) | ||
Theorem | imo72b2lem2 43588* | Lemma for imo72b2 43593. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → ∀𝑧 ∈ ℝ (abs‘(𝐹‘𝑧)) ≤ 𝐶) ⇒ ⊢ (𝜑 → sup((abs “ (𝐹 “ ℝ)), ℝ, < ) ≤ 𝐶) | ||
Theorem | suprlubrd 43589* | Natural deduction form of specialized suprlub 12203. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑧 ∈ 𝐴 𝐵 < 𝑧) ⇒ ⊢ (𝜑 → 𝐵 < sup(𝐴, ℝ, < )) | ||
Theorem | imo72b2lem1 43590* | Lemma for imo72b2 43593. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ (𝐹‘𝑥) ≠ 0) & ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1) ⇒ ⊢ (𝜑 → 0 < sup((abs “ (𝐹 “ ℝ)), ℝ, < )) | ||
Theorem | lemuldiv3d 43591 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → (𝐵 · 𝐴) ≤ 𝐶) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐵 ≤ (𝐶 / 𝐴)) | ||
Theorem | lemuldiv4d 43592 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐵 ≤ (𝐶 / 𝐴)) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 · 𝐴) ≤ 𝐶) | ||
Theorem | imo72b2 43593* | IMO 1972 B2. (14th International Mathematical Olympiad in Poland, problem B2). (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐺:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∀𝑢 ∈ ℝ ∀𝑣 ∈ ℝ ((𝐹‘(𝑢 + 𝑣)) + (𝐹‘(𝑢 − 𝑣))) = (2 · ((𝐹‘𝑢) · (𝐺‘𝑣)))) & ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ (𝐹‘𝑥) ≠ 0) ⇒ ⊢ (𝜑 → (abs‘(𝐺‘𝐵)) ≤ 1) | ||
This section formalizes theorems necessary to reproduce the equality and inequality generator described in "Neural Theorem Proving on Inequality Problems" http://aitp-conference.org/2020/abstract/paper_18.pdf. Other theorems required: 0red 11242 1red 11240 readdcld 11268 remulcld 11269 eqcomd 2734. | ||
Theorem | int-addcomd 43594 | AdditionCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 + 𝐶) = (𝐶 + 𝐴)) | ||
Theorem | int-addassocd 43595 | AdditionAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + 𝐷)) | ||
Theorem | int-addsimpd 43596 | AdditionSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 0 = (𝐴 − 𝐵)) | ||
Theorem | int-mulcomd 43597 | MultiplicationCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · 𝐶) = (𝐶 · 𝐴)) | ||
Theorem | int-mulassocd 43598 | MultiplicationAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · 𝐷)) | ||
Theorem | int-mulsimpd 43599 | MultiplicationSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → 1 = (𝐴 / 𝐵)) | ||
Theorem | int-leftdistd 43600 | AdditionMultiplicationLeftDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ((𝐶 + 𝐷) · 𝐵) = ((𝐶 · 𝐴) + (𝐷 · 𝐴))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |