P. 454 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 45301-45400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ntrneik13 45301*	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 45302*	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 45303*	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 45304*	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 45305	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 45306	The relative complement of the class 𝑆 exists as a subset of the base set. (Contributed by RP, 26-Jun-2021.)
⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    ⇒   ⊢ (𝜑 → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵)
Theorem	clsneif1o 45307*	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-1onto(𝒫 𝒫 𝐵 ↑m 𝐵))
Theorem	clsneicnv 45308*	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 45309*	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 45310*	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 45311*	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 45312*	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 45313*	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 45314*	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 45315	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 45316	The relative complement of the class 𝑆 exists as a subset of the base set. (Contributed by RP, 26-Jun-2021.)
⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    ⇒   ⊢ (𝜑 → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵)
Theorem	neicvgf1o 45317*	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-1onto(𝒫 𝒫 𝐵 ↑m 𝐵))
Theorem	neicvgnvo 45318*	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 45319*	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 45320*	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 45321*	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 45322*	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 45323*	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 45324*	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 45325	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 45326	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 45327	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 45328	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 45329	The closure function is a map from the powerset of the base set to itself. This is less precise than clsf 23399. (Contributed by RP, 22-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐾:𝒫 𝑋⟶𝒫 𝑋)
Theorem	clselmap 45330	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 45331*	The interior and closure operators on a topology are duals of each other. See also kur14lem2 36152. (Contributed by RP, 21-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝑋)    ⇒   ⊢ (𝐽 ∈ Top → 𝐼 = (𝐷‘𝐾))
Theorem	dssmapclsntr 45332*	The closure and interior operators on a topology are duals of each other. See also kur14lem2 36152. (Contributed by RP, 22-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝑋)    ⇒   ⊢ (𝐽 ∈ Top → 𝐾 = (𝐷‘𝐼))
21.40.7.3  Generic Neighborhood Spaces Any neighborhood space is an open set topology and any open set topology is a neighborhood space. Seifert and Threlfall define a generic neighborhood space which is a superset of what is now generally used and related concepts and the following will show that those definitions apply to elements of Top. Seifert and Threlfall do not allow neighborhood spaces on the empty set while sn0top 23350 is an example of a topology with an empty base set. This divergence is unlikely to pose serious problems.
Theorem	gneispa 45333*	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 45334*	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 45335*	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 45336*	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 45337*	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 45338*	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 45339*	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 45340*	A generic neighborhood space is a function. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → Fun 𝐹)
Theorem	gneispacern 45341*	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 45342*	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 45343*	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 45344*	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 45345*	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 45346*	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 45347*	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 45348*	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 45349*	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 𝐹 ∧ 𝑁 ⊆ 𝑆)) → 𝑆 ∈ (𝐹‘𝑃))
21.40.8  Exploring Higher Homotopy via Kerodon See https://kerodon.net/ for a work in progress by Jacob Lurie.
21.40.8.1  Simplicial Sets See https://kerodon.net/tag/0004 for introduction to the topological simplex of dimension 𝑁.
Theorem	k0004lem1 45350	Application of ssin 4138 to range of a function. (Contributed by RP, 1-Apr-2021.)
⊢ (𝐷 = (𝐵 ∩ 𝐶) → ((𝐹:𝐴⟶𝐵 ∧ (𝐹 “ 𝐴) ⊆ 𝐶) ↔ 𝐹:𝐴⟶𝐷))
Theorem	k0004lem2 45351	A mapping with a particular restricted range is also a mapping to that range. (Contributed by RP, 1-Apr-2021.)
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝐵) → ((𝐹 ∈ (𝐵 ↑m 𝐴) ∧ (𝐹 “ 𝐴) ⊆ 𝐶) ↔ 𝐹 ∈ (𝐶 ↑m 𝐴)))
Theorem	k0004lem3 45352	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 45353*	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 (0...𝑛)) ∣ Σ𝑘 ∈ (0...𝑛)(𝑡‘𝑘) = 1})    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐴‘𝑁) = {𝑡 ∈ ((0[,]1) ↑m (0...𝑁)) ∣ Σ𝑘 ∈ (0...𝑁)(𝑡‘𝑘) = 1})
Theorem	k0004ss1 45354*	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 (0...𝑛)) ∣ Σ𝑘 ∈ (0...𝑛)(𝑡‘𝑘) = 1})    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐴‘𝑁) ⊆ (ℝ ↑m (0...𝑁)))
Theorem	k0004ss2 45355*	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 (0...𝑛)) ∣ Σ𝑘 ∈ (0...𝑛)(𝑡‘𝑘) = 1})    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐴‘𝑁) ⊆ (Base‘(ℝ^‘(0...𝑁))))
Theorem	k0004ss3 45356*	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 (0...𝑛)) ∣ Σ𝑘 ∈ (0...𝑛)(𝑡‘𝑘) = 1})    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐴‘𝑁) ⊆ (Base‘(𝔼hil‘(𝑁 + 1))))
Theorem	k0004val0 45357*	The topological simplex of dimension 0 is a singleton. (Contributed by RP, 2-Apr-2021.)
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑m (0...𝑛)) ∣ Σ𝑘 ∈ (0...𝑛)(𝑡‘𝑘) = 1})    ⇒   ⊢ (𝐴‘0) = {⟨“1”⟩}
21.41  Mathbox for Stanislas Polu
Theorem	inductionexd 45358	Simple induction example. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝑁 ∈ ℕ → 3 ∥ ((4↑𝑁) + 5))
21.41.1  IMO Problems
21.41.1.1  IMO 1972 B2
Theorem	wwlemuld 45359	Natural deduction form of lemul2d 13238. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))    &   ⊢ (𝜑 → 0 < 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	leeq1d 45360	Specialization of breq1d 5116 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐵 ≤ 𝐶)
Theorem	leeq2d 45361	Specialization of breq2d 5118 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐷)
Theorem	absmulrposd 45362	Specialization of absmuld with absidd 15622. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 · 𝐵)) = (𝐴 · (abs‘𝐵)))
Theorem	imadisjld 45363	Natural dduction form of one side of imadisj 6090. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → (dom 𝐴 ∩ 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐵) = ∅)
Theorem	wnefimgd 45364	The image of a mapping from A is nonempty if A is nonempty. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐹 “ 𝐴) ≠ ∅)
Theorem	fco2d 45365	Natural deduction form of fco2 6761. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐴⟶𝐶)
Theorem	wfximgfd 45366	The value of a function on its domain is in the image of the function. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘𝐶) ∈ (𝐹 “ 𝐴))
Theorem	extoimad 45367*	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 45368*	Lemma for imo72b2 45375. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐺:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘(𝐴 + 𝐵)) + (𝐹‘(𝐴 − 𝐵))) = (2 · ((𝐹‘𝐴) · (𝐺‘𝐵))))    &   ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1)    ⇒   ⊢ (𝜑 → ((abs‘(𝐹‘𝐴)) · (abs‘(𝐺‘𝐵))) ≤ sup((abs “ (𝐹 “ ℝ)), ℝ, < ))
Theorem	suprleubrd 45369*	Natural deduction form of specialized suprleub 12313. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝐵)    ⇒   ⊢ (𝜑 → sup(𝐴, ℝ, < ) ≤ 𝐵)
Theorem	imo72b2lem2 45370*	Lemma for imo72b2 45375. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑧 ∈ ℝ (abs‘(𝐹‘𝑧)) ≤ 𝐶)    ⇒   ⊢ (𝜑 → sup((abs “ (𝐹 “ ℝ)), ℝ, < ) ≤ 𝐶)
Theorem	suprlubrd 45371*	Natural deduction form of specialized suprlub 12311. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑧 ∈ 𝐴 𝐵 < 𝑧)    ⇒   ⊢ (𝜑 → 𝐵 < sup(𝐴, ℝ, < ))
Theorem	imo72b2lem1 45372*	Lemma for imo72b2 45375. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (𝐹‘𝑥) ≠ 0)    &   ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1)    ⇒   ⊢ (𝜑 → 0 < sup((abs “ (𝐹 “ ℝ)), ℝ, < ))
Theorem	lemuldiv3d 45373	'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → (𝐵 · 𝐴) ≤ 𝐶)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐵 ≤ (𝐶 / 𝐴))
Theorem	lemuldiv4d 45374	'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐵 ≤ (𝐶 / 𝐴))    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐵 · 𝐴) ≤ 𝐶)
Theorem	imo72b2 45375*	IMO 1972 B2. (14th International Mathematical Olympiad in Poland, problem B2). (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐺:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑢 ∈ ℝ ∀𝑣 ∈ ℝ ((𝐹‘(𝑢 + 𝑣)) + (𝐹‘(𝑢 − 𝑣))) = (2 · ((𝐹‘𝑢) · (𝐺‘𝑣))))    &   ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (𝐹‘𝑥) ≠ 0)    ⇒   ⊢ (𝜑 → (abs‘(𝐺‘𝐵)) ≤ 1)
21.41.2  INT Inequalities Proof Generator This section formalizes theorems necessary to reproduce the equality and inequality generator described in "Neural Theorem Proving on Inequality Problems" http://aitp-conference.org/2020/abstract/paper_18.pdf. Other theorems required: 0red 11341 1red 11339 readdcld 11368 remulcld 11369 eqcomd 2769.
Theorem	int-addcomd 45376	AdditionCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐵 + 𝐶) = (𝐶 + 𝐴))
Theorem	int-addassocd 45377	AdditionAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐵 + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + 𝐷))
Theorem	int-addsimpd 45378	AdditionSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 0 = (𝐴 − 𝐵))
Theorem	int-mulcomd 45379	MultiplicationCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐵 · 𝐶) = (𝐶 · 𝐴))
Theorem	int-mulassocd 45380	MultiplicationAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐵 · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · 𝐷))
Theorem	int-mulsimpd 45381	MultiplicationSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → 1 = (𝐴 / 𝐵))
Theorem	int-leftdistd 45382	AdditionMultiplicationLeftDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ((𝐶 + 𝐷) · 𝐵) = ((𝐶 · 𝐴) + (𝐷 · 𝐴)))
Theorem	int-rightdistd 45383	AdditionMultiplicationRightDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐵 · (𝐶 + 𝐷)) = ((𝐴 · 𝐶) + (𝐴 · 𝐷)))
Theorem	int-sqdefd 45384	SquareDefinition generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐴↑2))
Theorem	int-mul11d 45385	First MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 · 1) = 𝐵)
Theorem	int-mul12d 45386	Second MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (1 · 𝐴) = 𝐵)
Theorem	int-add01d 45387	First AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 + 0) = 𝐵)
Theorem	int-add02d 45388	Second AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (0 + 𝐴) = 𝐵)
Theorem	int-sqgeq0d 45389	SquareGEQZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵))
Theorem	int-eqprincd 45390	PrincipleOfEquality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐶) = (𝐵 + 𝐷))
Theorem	int-eqtransd 45391	EqualityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	int-eqmvtd 45392	EquMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷))    ⇒   ⊢ (𝜑 → 𝐶 = (𝐵 − 𝐷))
Theorem	int-eqineqd 45393	EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≤ 𝐴)
Theorem	int-ineqmvtd 45394	IneqMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷))    ⇒   ⊢ (𝜑 → (𝐵 − 𝐷) ≤ 𝐶)
Theorem	int-ineq1stprincd 45395	FirstPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐷 ≤ 𝐶)    ⇒   ⊢ (𝜑 → (𝐵 + 𝐷) ≤ (𝐴 + 𝐶))
Theorem	int-ineq2ndprincd 45396	SecondPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    ⇒   ⊢ (𝜑 → (𝐵 · 𝐶) ≤ (𝐴 · 𝐶))
Theorem	int-ineqtransd 45397	InequalityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ≤ 𝐴)
21.41.3  N-Digit Addition Proof Generator This section formalizes theorems used in an n-digit addition proof generator. Other theorems required: deccl 12859 addcomli 11532 00id 11515 addridi 11527 addlidi 11528 eqid 2763 dec0h 12871 decadd 12903 decaddc 12904.
Theorem	unitadd 45398	Theorem used in conjunction with decaddc 12904 to absorb carry when generating n-digit addition synthetic proofs. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝐴 + 𝐵) = 𝐹    &   ⊢ (𝐶 + 1) = 𝐵    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    ⇒   ⊢ ((𝐴 + 𝐶) + 1) = 𝐹
21.41.4  AM-GM (for k = 2,3,4)
Theorem	gsumws3 45399	Valuation of a length 3 word in a monoid. (Contributed by Stanislas Polu, 9-Sep-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵))) → (𝐺 Σg ⟨“𝑆𝑇𝑈”⟩) = (𝑆 + (𝑇 + 𝑈)))
Theorem	gsumws4 45400	Valuation of a length 4 word in a monoid. (Contributed by Stanislas Polu, 10-Sep-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ (𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)))) → (𝐺 Σg ⟨“𝑆𝑇𝑈𝑉”⟩) = (𝑆 + (𝑇 + (𝑈 + 𝑉))))