P. 219 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21801-21900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tlmtps 21801	A topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopSp)
Theorem	tlmlmod 21802	A topological module is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ LMod)
Theorem	tlmtrg 21803	The scalar ring of a topological module is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopRing)
Theorem	tlmscatps 21804	The scalar ring of a topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopSp)
Theorem	istvc 21805	A topological vector space is a topological module over a topological division ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ TopVec ↔ (𝑊 ∈ TopMod ∧ 𝐹 ∈ TopDRing))
Theorem	tvctdrg 21806	The scalar field of a topological vector space is a topological division ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ TopVec → 𝐹 ∈ TopDRing)
Theorem	cnmpt1vsca 21807*	Continuity of scalar multiplication; analogue of cnmpt12f 21279 which cannot be used directly because ·𝑠 is not a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐾 = (TopOpen‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ TopMod)    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐿 Cn 𝐾))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐿 Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝐿 Cn 𝐽))
Theorem	cnmpt2vsca 21808*	Continuity of scalar multiplication; analogue of cnmpt22f 21288 which cannot be used directly because ·𝑠 is not a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐾 = (TopOpen‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ TopMod)    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐿 ×t 𝑀) Cn 𝐾))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐿 ×t 𝑀) Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴 · 𝐵)) ∈ ((𝐿 ×t 𝑀) Cn 𝐽))
Theorem	tlmtgp 21809	A topological vector space is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopGrp)
Theorem	tvctlm 21810	A topological vector space is a topological module. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ TopMod)
Theorem	tvclmod 21811	A topological vector space is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ LMod)
Theorem	tvclvec 21812	A topological vector space is a vector space. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ LVec)
12.3  Uniform Structures and Spaces
12.3.1  Uniform structures
Syntax	cust 21813	Extend class notation with the class function of uniform structures.
class UnifOn
Definition	df-ust 21814*	Definition of a uniform structure. Definition 1 of [BourbakiTop1] p. II.1. A uniform structure is used to give a generalization of the idea of Cauchy's sequence. This definition is analogous to TopOn. Elements of an uniform structure are called entourages. (Contributed by FL, 29-May-2014.) (Revised by Thierry Arnoux, 15-Nov-2017.)
⊢ UnifOn = (𝑥 ∈ V ↦ {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))})
Theorem	ustfn 21815	The defined uniform structure as a function. (Contributed by Thierry Arnoux, 15-Nov-2017.)
⊢ UnifOn Fn V
Theorem	ustval 21816*	The class of all uniform structures for a base 𝑋. (Contributed by Thierry Arnoux, 15-Nov-2017.) (Revised by AV, 17-Sep-2021.)
⊢ (𝑋 ∈ 𝑉 → (UnifOn‘𝑋) = {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))})
Theorem	isust 21817*	The predicate "𝑈 is a uniform structure with base 𝑋." (Contributed by Thierry Arnoux, 15-Nov-2017.) (Revised by AV, 17-Sep-2021.)
⊢ (𝑋 ∈ 𝑉 → (𝑈 ∈ (UnifOn‘𝑋) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣 ∈ 𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣)))))
Theorem	ustssxp 21818	Entourages are subsets of the Cartesian product of the base set. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → 𝑉 ⊆ (𝑋 × 𝑋))
Theorem	ustssel 21819	A uniform structure is upward closed. Condition FI of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017.) (Proof shortened by AV, 17-Sep-2021.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ⊆ (𝑋 × 𝑋)) → (𝑉 ⊆ 𝑊 → 𝑊 ∈ 𝑈))
Theorem	ustbasel 21820	The full set is always an entourage. Condition FIIb of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) ∈ 𝑈)
Theorem	ustincl 21821	A uniform structure is closed under finite intersection. Condition FII of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 30-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ∈ 𝑈) → (𝑉 ∩ 𝑊) ∈ 𝑈)
Theorem	ustdiag 21822	The diagonal set is included in any entourage, i.e. any point is 𝑉 -close to itself. Condition UI of [BourbakiTop1] p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ( I ↾ 𝑋) ⊆ 𝑉)
Theorem	ustinvel 21823	If 𝑉 is an entourage, so is its inverse. Condition UII of [BourbakiTop1] p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ◡𝑉 ∈ 𝑈)
Theorem	ustexhalf 21824*	For each entourage 𝑉 there is an entourage 𝑤 that is "not more than half as large". Condition UIII of [BourbakiTop1] p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑉)
Theorem	ustrel 21825	The elements of uniform structures, called entourages, are relations. (Contributed by Thierry Arnoux, 15-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → Rel 𝑉)
Theorem	ustfilxp 21826	A uniform structure on a nonempty base is a filter. Remark 3 of [BourbakiTop1] p. II.2. (Contributed by Thierry Arnoux, 15-Nov-2017.)
⊢ ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → 𝑈 ∈ (Fil‘(𝑋 × 𝑋)))
Theorem	ustne0 21827	A uniform structure cannot be empty. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 ≠ ∅)
Theorem	ustssco 21828	In an uniform structure, any entourage 𝑉 is a subset of its composition with itself. (Contributed by Thierry Arnoux, 5-Jan-2018.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → 𝑉 ⊆ (𝑉 ∘ 𝑉))
Theorem	ustexsym 21829*	In an uniform structure, for any entourage 𝑉, there exists a smaller symmetrical entourage. (Contributed by Thierry Arnoux, 4-Jan-2018.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (◡𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑉))
Theorem	ustex2sym 21830*	In an uniform structure, for any entourage 𝑉, there exists a symmetrical entourage smaller than half 𝑉. (Contributed by Thierry Arnoux, 16-Jan-2018.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (◡𝑤 = 𝑤 ∧ (𝑤 ∘ 𝑤) ⊆ 𝑉))
Theorem	ustex3sym 21831*	In an uniform structure, for any entourage 𝑉, there exists a symmetrical entourage smaller than a third of 𝑉. (Contributed by Thierry Arnoux, 16-Jan-2018.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (◡𝑤 = 𝑤 ∧ (𝑤 ∘ (𝑤 ∘ 𝑤)) ⊆ 𝑉))
Theorem	ustref 21832	Any element of the base set is "near" itself, i.e. entourages are reflexive. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝐴 ∈ 𝑋) → 𝐴𝑉𝐴)
Theorem	ust0 21833	The unique uniform structure of the empty set is the empty set. Remark 3 of [BourbakiTop1] p. II.2. (Contributed by Thierry Arnoux, 15-Nov-2017.)
⊢ (UnifOn‘∅) = {{∅}}
Theorem	ustn0 21834	The empty set is not an uniform structure. (Contributed by Thierry Arnoux, 3-Dec-2017.)
⊢ ¬ ∅ ∈ ∪ ran UnifOn
Theorem	ustund 21835	If two intersecting sets 𝐴 and 𝐵 are both small in 𝑉, their union is small in (𝑉↑2). Proposition 1 of [BourbakiTop1] p. II.12. This proposition actually does not require any axiom of the definition of uniform structures. (Contributed by Thierry Arnoux, 17-Nov-2017.)
⊢ (𝜑 → (𝐴 × 𝐴) ⊆ 𝑉)    &   ⊢ (𝜑 → (𝐵 × 𝐵) ⊆ 𝑉)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ≠ ∅)    ⇒   ⊢ (𝜑 → ((𝐴 ∪ 𝐵) × (𝐴 ∪ 𝐵)) ⊆ (𝑉 ∘ 𝑉))
Theorem	ustelimasn 21836	Any point 𝐴 is near enough to itself. (Contributed by Thierry Arnoux, 18-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ (𝑉 “ {𝐴}))
Theorem	ustneism 21837	For a point 𝐴 in 𝑋, (𝑉 “ {𝐴}) is small enough in (𝑉 ∘ ◡𝑉). This proposition actually does not require any axiom of the definition of uniform structures. (Contributed by Thierry Arnoux, 18-Nov-2017.)
⊢ ((𝑉 ⊆ (𝑋 × 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑉 “ {𝐴}) × (𝑉 “ {𝐴})) ⊆ (𝑉 ∘ ◡𝑉))
Theorem	elrnust 21838	First direction for ustbas 21841. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 ∈ ∪ ran UnifOn)
Theorem	ustbas2 21839	Second direction for ustbas 21841. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = dom ∪ 𝑈)
Theorem	ustuni 21840	The set union of a uniform structure is the Cartesian product of its base. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ 𝑈 = (𝑋 × 𝑋))
Theorem	ustbas 21841	Recover the base of an uniform structure 𝑈. ∪ ran UnifOn is to UnifOn what Top is to TopOn. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ 𝑋 = dom ∪ 𝑈    ⇒   ⊢ (𝑈 ∈ ∪ ran UnifOn ↔ 𝑈 ∈ (UnifOn‘𝑋))
Theorem	ustimasn 21842	Lemma for ustuqtop 21860. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋) → (𝑉 “ {𝑃}) ⊆ 𝑋)
Theorem	trust 21843	The trace of a uniform structure 𝑈 on a subset 𝐴 is a uniform structure on 𝐴. Definition 3 of [BourbakiTop1] p. II.9. (Contributed by Thierry Arnoux, 2-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴))
12.3.2  The topology induced by an uniform structure
Syntax	cutop 21844	Extend class notation with the function inducing a topology from a uniform structure.
class unifTop
Definition	df-utop 21845*	Definition of a topology induced by a uniform structure. Definition 3 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017.)
⊢ unifTop = (𝑢 ∈ ∪ ran UnifOn ↦ {𝑎 ∈ 𝒫 dom ∪ 𝑢 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎})
Theorem	utopval 21846*	The topology induced by a uniform structure 𝑈. (Contributed by Thierry Arnoux, 30-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎})
Theorem	elutop 21847*	Open sets in the topology induced by an uniform structure 𝑈 on 𝑋 (Contributed by Thierry Arnoux, 30-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ (unifTop‘𝑈) ↔ (𝐴 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴)))
Theorem	utoptop 21848	The topology induced by a uniform structure 𝑈 is a topology. (Contributed by Thierry Arnoux, 30-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ Top)
Theorem	utopbas 21849	The base of the topology induced by a uniform structure 𝑈. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪ (unifTop‘𝑈))
Theorem	utoptopon 21850	Topology induced by a uniform structure 𝑈 with its base set. (Contributed by Thierry Arnoux, 5-Jan-2018.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ (TopOn‘𝑋))
Theorem	restutop 21851	Restriction of a topology induced by an uniform structure. (Contributed by Thierry Arnoux, 12-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((unifTop‘𝑈) ↾t 𝐴) ⊆ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))))
Theorem	restutopopn 21852	The restriction of the topology induced by an uniform structure to an open set. (Contributed by Thierry Arnoux, 16-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → ((unifTop‘𝑈) ↾t 𝐴) = (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))))
Theorem	ustuqtoplem 21853*	Lemma for ustuqtop 21860. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝐴 ∈ 𝑉) → (𝐴 ∈ (𝑁‘𝑃) ↔ ∃𝑤 ∈ 𝑈 𝐴 = (𝑤 “ {𝑃})))
Theorem	ustuqtop0 21854*	Lemma for ustuqtop 21860. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑁:𝑋⟶𝒫 𝒫 𝑋)
Theorem	ustuqtop1 21855*	Lemma for ustuqtop 21860, similar to ssnei2 20730. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))
Theorem	ustuqtop2 21856*	Lemma for ustuqtop 21860. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))
Theorem	ustuqtop3 21857*	Lemma for ustuqtop 21860, similar to elnei 20725. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)
Theorem	ustuqtop4 21858*	Lemma for ustuqtop 21860. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
Theorem	ustuqtop5 21859*	Lemma for ustuqtop 21860. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝))
Theorem	ustuqtop 21860*	For a given uniform structure 𝑈 on a set 𝑋, there is a unique topology 𝑗 such that the set ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) is the filter of the neighborhoods of 𝑝 for that topology. Proposition 1 of [BourbakiTop1] p. II.3. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∃!𝑗 ∈ (TopOn‘𝑋)∀𝑝 ∈ 𝑋 (𝑁‘𝑝) = ((nei‘𝑗)‘{𝑝}))
Theorem	utopsnneiplem 21861*	The neighborhoods of a point 𝑃 for the topology induced by an uniform space 𝑈. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝐽 = (unifTop‘𝑈)    &   ⊢ 𝐾 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}    &   ⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))
Theorem	utopsnneip 21862*	The neighborhoods of a point 𝑃 for the topology induced by an uniform space 𝑈. (Contributed by Thierry Arnoux, 13-Jan-2018.)
⊢ 𝐽 = (unifTop‘𝑈)    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))
Theorem	utopsnnei 21863	Images of singletons by entourages 𝑉 are neighborhoods of those singletons. (Contributed by Thierry Arnoux, 13-Jan-2018.)
⊢ 𝐽 = (unifTop‘𝑈)    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋) → (𝑉 “ {𝑃}) ∈ ((nei‘𝐽)‘{𝑃}))
Theorem	utop2nei 21864	For any symmetrical entourage 𝑉 and any relation 𝑀, build a neighborhood of 𝑀. First part of proposition 2 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 14-Jan-2018.)
⊢ 𝐽 = (unifTop‘𝑈)    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×t 𝐽))‘𝑀))
Theorem	utop3cls 21865	Relation between a topological closure and a symmetric entourage in an uniform space. Second part of proposition 2 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 17-Jan-2018.)
⊢ 𝐽 = (unifTop‘𝑈)    ⇒   ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) → ((cls‘(𝐽 ×t 𝐽))‘𝑀) ⊆ (𝑉 ∘ (𝑀 ∘ 𝑉)))
Theorem	utopreg 21866	All Hausdorff uniform spaces are regular. Proposition 3 of [BourbakiTop1] p. II.5. (Contributed by Thierry Arnoux, 16-Jan-2018.)
⊢ 𝐽 = (unifTop‘𝑈)    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐽 ∈ Haus) → 𝐽 ∈ Reg)
12.3.3  Uniform Spaces
Syntax	cuss 21867	Extend class notation with the Uniform Structure extractor function.
class UnifSt
Syntax	cusp 21868	Extend class notation with the class of uniform spaces.
class UnifSp
Syntax	ctus 21869	Extend class notation with the function mapping a uniform structure to a uniform space.
class toUnifSp
Definition	df-uss 21870	Define the uniform structure extractor function. Similarly with df-topn 15907 this differs from df-unif 15792 when a structure has been restricted using df-ress 15702; in this case the UnifSet component will still have a uniform set over the larger set, and this function fixes this by restricting the uniform set as well. (Contributed by Thierry Arnoux, 1-Dec-2017.)
⊢ UnifSt = (𝑓 ∈ V ↦ ((UnifSet‘𝑓) ↾t ((Base‘𝑓) × (Base‘𝑓))))
Definition	df-usp 21871	Definition of a uniform space, i.e. a base set with an uniform structure and its induced topology. Derived from definition 3 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017.)
⊢ UnifSp = {𝑓 ∣ ((UnifSt‘𝑓) ∈ (UnifOn‘(Base‘𝑓)) ∧ (TopOpen‘𝑓) = (unifTop‘(UnifSt‘𝑓)))}
Definition	df-tus 21872	Define the function mapping a uniform structure to a uniform space. (Contributed by Thierry Arnoux, 17-Nov-2017.)
⊢ toUnifSp = (𝑢 ∈ ∪ ran UnifOn ↦ ({⟨(Base‘ndx), dom ∪ 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩))
Theorem	ussval 21873	The uniform structure on uniform space 𝑊. This proof uses a trick with fvprc 6097 to avoid requiring 𝑊 to be a set. (Contributed by Thierry Arnoux, 3-Dec-2017.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑈 = (UnifSet‘𝑊)    ⇒   ⊢ (𝑈 ↾t (𝐵 × 𝐵)) = (UnifSt‘𝑊)
Theorem	ussid 21874	In case the base of the UnifSt element of the uniform space is the base of its element structure, then UnifSt does not restrict it further. (Contributed by Thierry Arnoux, 4-Dec-2017.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑈 = (UnifSet‘𝑊)    ⇒   ⊢ ((𝐵 × 𝐵) = ∪ 𝑈 → 𝑈 = (UnifSt‘𝑊))
Theorem	isusp 21875	The predicate 𝑊 is a uniform space. (Contributed by Thierry Arnoux, 4-Dec-2017.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑈 = (UnifSt‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    ⇒   ⊢ (𝑊 ∈ UnifSp ↔ (𝑈 ∈ (UnifOn‘𝐵) ∧ 𝐽 = (unifTop‘𝑈)))
Theorem	ressunif 21876	UnifSet is unaffected by restriction. (Contributed by Thierry Arnoux, 7-Dec-2017.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝑈 = (UnifSet‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝑈 = (UnifSet‘𝐻))
Theorem	ressuss 21877	Value of the uniform structure of a restricted space. (Contributed by Thierry Arnoux, 12-Dec-2017.)
⊢ (𝐴 ∈ 𝑉 → (UnifSt‘(𝑊 ↾s 𝐴)) = ((UnifSt‘𝑊) ↾t (𝐴 × 𝐴)))
Theorem	ressust 21878	The uniform structure of a restricted space. (Contributed by Thierry Arnoux, 22-Jan-2018.)
⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 𝑇 = (UnifSt‘(𝑊 ↾s 𝐴))    ⇒   ⊢ ((𝑊 ∈ UnifSp ∧ 𝐴 ⊆ 𝑋) → 𝑇 ∈ (UnifOn‘𝐴))
Theorem	ressusp 21879	The restriction of a uniform topological space to an open set is a uniform space. (Contributed by Thierry Arnoux, 16-Dec-2017.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    ⇒   ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (𝑊 ↾s 𝐴) ∈ UnifSp)
Theorem	tusval 21880	The value of the uniform space mapping function. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (toUnifSp‘𝑈) = ({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩))
Theorem	tuslem 21881	Lemma for tusbas 21882, tusunif 21883, and tustopn 21885. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ 𝐾 = (toUnifSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝑈 = (UnifSet‘𝐾) ∧ (unifTop‘𝑈) = (TopOpen‘𝐾)))
Theorem	tusbas 21882	The base set of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ 𝐾 = (toUnifSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = (Base‘𝐾))
Theorem	tusunif 21883	The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ 𝐾 = (toUnifSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSet‘𝐾))
Theorem	tususs 21884	The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017.)
⊢ 𝐾 = (toUnifSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSt‘𝐾))
Theorem	tustopn 21885	The topology induced by a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ 𝐾 = (toUnifSp‘𝑈)    &   ⊢ 𝐽 = (unifTop‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = (TopOpen‘𝐾))
Theorem	tususp 21886	A constructed uniform space is an uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ 𝐾 = (toUnifSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 ∈ UnifSp)
Theorem	tustps 21887	A constructed uniform space is a topological space. (Contributed by Thierry Arnoux, 25-Jan-2018.)
⊢ 𝐾 = (toUnifSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 ∈ TopSp)
Theorem	uspreg 21888	If a uniform space is Hausdorff, it is regular. Proposition 3 of [BourbakiTop1] p. II.5. (Contributed by Thierry Arnoux, 4-Jan-2018.)
⊢ 𝐽 = (TopOpen‘𝑊)    ⇒   ⊢ ((𝑊 ∈ UnifSp ∧ 𝐽 ∈ Haus) → 𝐽 ∈ Reg)
12.3.4  Uniform continuity
Syntax	cucn 21889	Extend class notation with the uniform continuity operation.
class Cnu
Definition	df-ucn 21890*	Define a function on two uniform structures which value is the set of uniformly continuous functions from the first uniform structure to the second. A function 𝑓 is uniformly continuous if, roughly speaking, it is possible to guarantee that (𝑓‘𝑥) and (𝑓‘𝑦) be as close to each other as we please by requiring only that 𝑥 and 𝑦 are sufficiently close to each other; unlike ordinary continuity, the maximum distance between (𝑓‘𝑥) and (𝑓‘𝑦) cannot depend on 𝑥 and 𝑦 themselves. This formulation is the definition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ Cnu = (𝑢 ∈ ∪ ran UnifOn, 𝑣 ∈ ∪ ran UnifOn ↦ {𝑓 ∈ (dom ∪ 𝑣 ↑𝑚 dom ∪ 𝑢) ∣ ∀𝑠 ∈ 𝑣 ∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪ 𝑢∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})
Theorem	ucnval 21891*	The set of all uniformly continuous function from uniform space 𝑈 to uniform space 𝑉. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝑈 Cnu𝑉) = {𝑓 ∈ (𝑌 ↑𝑚 𝑋) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})
Theorem	isucn 21892*	The predicate "𝐹 is a uniformly continuous function from uniform space 𝑈 to uniform space 𝑉." (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))))
Theorem	isucn2 21893*	The predicate "𝐹 is a uniformly continuous function from uniform space 𝑈 to uniform space 𝑉." , expressed with filter bases for the entourages. (Contributed by Thierry Arnoux, 26-Jan-2018.)
⊢ 𝑈 = ((𝑋 × 𝑋)filGen𝑅)    &   ⊢ 𝑉 = ((𝑌 × 𝑌)filGen𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝑅 ∈ (fBas‘(𝑋 × 𝑋)))    &   ⊢ (𝜑 → 𝑆 ∈ (fBas‘(𝑌 × 𝑌)))    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑠 ∈ 𝑆 ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))))
Theorem	ucnimalem 21894*	Reformulate the 𝐺 function as a mapping with one variable. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)    ⇒   ⊢ 𝐺 = (𝑝 ∈ (𝑋 × 𝑋) ↦ ⟨(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))⟩)
Theorem	ucnima 21895*	An equivalent statement of the definition of uniformly continuous function. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ 𝑈 (𝐺 “ 𝑟) ⊆ 𝑊)
Theorem	ucnprima 21896*	The preimage by a uniformly continuous function 𝐹 of an entourage 𝑊 of 𝑌 is an entourage of 𝑋. Note of the definition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)    ⇒   ⊢ (𝜑 → (◡𝐺 “ 𝑊) ∈ 𝑈)
Theorem	iducn 21897	The identity is uniformly continuous from a uniform structure to itself. Example 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ( I ↾ 𝑋) ∈ (𝑈 Cnu𝑈))
Theorem	cstucnd 21898	A constant function is uniformly continuous. Deduction form. Example 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑌)    ⇒   ⊢ (𝜑 → (𝑋 × {𝐴}) ∈ (𝑈 Cnu𝑉))
Theorem	ucncn 21899	Uniform continuity implies continuity. Deduction form. Proposition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 30-Nov-2017.)
⊢ 𝐽 = (TopOpen‘𝑅)    &   ⊢ 𝐾 = (TopOpen‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ UnifSp)    &   ⊢ (𝜑 → 𝑆 ∈ UnifSp)    &   ⊢ (𝜑 → 𝑅 ∈ TopSp)    &   ⊢ (𝜑 → 𝑆 ∈ TopSp)    &   ⊢ (𝜑 → 𝐹 ∈ ((UnifSt‘𝑅) Cnu(UnifSt‘𝑆)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))
12.3.5  Cauchy filters in uniform spaces
Syntax	ccfilu 21900	Extend class notation with the set of Cauchy filter bases.
class CauFilu