P. 243 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24201-24300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ustuqtop5 24201*	Lemma for ustuqtop 24202. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝))
Theorem	ustuqtop 24202*	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 24203*	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 24204*	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 24205	Images of singletons by entourages 𝑉 are neighborhoods of those singletons. (Contributed by Thierry Arnoux, 13-Jan-2018.)
⊢ 𝐽 = (unifTop‘𝑈)    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋) → (𝑉 “ {𝑃}) ∈ ((nei‘𝐽)‘{𝑃}))
Theorem	utop2nei 24206	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 24207	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 24208	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 24209	Extend class notation with the Uniform Structure extractor function.
class UnifSt
Syntax	cusp 24210	Extend class notation with the class of uniform spaces.
class UnifSp
Syntax	ctus 24211	Extend class notation with the function mapping a uniform structure to a uniform space.
class toUnifSp
Definition	df-uss 24212	Define the uniform structure extractor function. Similarly with df-topn 17355 this differs from df-unif 17212 when a structure has been restricted using df-ress 17170; 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 24213	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 24214	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 24215	The uniform structure on uniform space 𝑊. This proof uses a trick with fvprc 6834 to avoid requiring 𝑊 to be a set. (Contributed by Thierry Arnoux, 3-Dec-2017.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑈 = (UnifSet‘𝑊)    ⇒   ⊢ (𝑈 ↾t (𝐵 × 𝐵)) = (UnifSt‘𝑊)
Theorem	ussid 24216	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 24217	The predicate 𝑊 is a uniform space. (Contributed by Thierry Arnoux, 4-Dec-2017.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑈 = (UnifSt‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    ⇒   ⊢ (𝑊 ∈ UnifSp ↔ (𝑈 ∈ (UnifOn‘𝐵) ∧ 𝐽 = (unifTop‘𝑈)))
Theorem	ressuss 24218	Value of the uniform structure of a restricted space. (Contributed by Thierry Arnoux, 12-Dec-2017.)
⊢ (𝐴 ∈ 𝑉 → (UnifSt‘(𝑊 ↾s 𝐴)) = ((UnifSt‘𝑊) ↾t (𝐴 × 𝐴)))
Theorem	ressust 24219	The uniform structure of a restricted space. (Contributed by Thierry Arnoux, 22-Jan-2018.)
⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 𝑇 = (UnifSt‘(𝑊 ↾s 𝐴))    ⇒   ⊢ ((𝑊 ∈ UnifSp ∧ 𝐴 ⊆ 𝑋) → 𝑇 ∈ (UnifOn‘𝐴))
Theorem	ressusp 24220	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 24221	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 24222	Lemma for tusbas 24223, tusunif 24224, and tustopn 24226. (Contributed by Thierry Arnoux, 5-Dec-2017.) (Proof shortened by AV, 28-Oct-2024.)
⊢ 𝐾 = (toUnifSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝑈 = (UnifSet‘𝐾) ∧ (unifTop‘𝑈) = (TopOpen‘𝐾)))
Theorem	tusbas 24223	The base set of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ 𝐾 = (toUnifSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = (Base‘𝐾))
Theorem	tusunif 24224	The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ 𝐾 = (toUnifSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSet‘𝐾))
Theorem	tususs 24225	The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017.)
⊢ 𝐾 = (toUnifSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSt‘𝐾))
Theorem	tustopn 24226	The topology induced by a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ 𝐾 = (toUnifSp‘𝑈)    &   ⊢ 𝐽 = (unifTop‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = (TopOpen‘𝐾))
Theorem	tususp 24227	A constructed uniform space is an uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ 𝐾 = (toUnifSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 ∈ UnifSp)
Theorem	tustps 24228	A constructed uniform space is a topological space. (Contributed by Thierry Arnoux, 25-Jan-2018.)
⊢ 𝐾 = (toUnifSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 ∈ TopSp)
Theorem	uspreg 24229	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 24230	Extend class notation with the uniform continuity operation.
class Cnu
Definition	df-ucn 24231*	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 ∪ 𝑣 ↑m dom ∪ 𝑢) ∣ ∀𝑠 ∈ 𝑣 ∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪ 𝑢∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})
Theorem	ucnval 24232*	The set of all uniformly continuous function from uniform space 𝑈 to uniform space 𝑉. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝑈 Cnu𝑉) = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})
Theorem	isucn 24233*	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 24234*	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 24235*	Reformulate the 𝐺 function as a mapping with one variable. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)    ⇒   ⊢ 𝐺 = (𝑝 ∈ (𝑋 × 𝑋) ↦ ⟨(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))⟩)
Theorem	ucnima 24236*	An equivalent statement of the definition of uniformly continuous function. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ 𝑈 (𝐺 “ 𝑟) ⊆ 𝑊)
Theorem	ucnprima 24237*	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 24238	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 24239	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 24240	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 24241	Extend class notation with the set of Cauchy filter bases.
class CauFilu
Definition	df-cfilu 24242*	Define the set of Cauchy filter bases on a uniform space. A Cauchy filter base is a filter base on the set such that for every entourage 𝑣, there is an element 𝑎 of the filter "small enough in 𝑣 " i.e. such that every pair {𝑥, 𝑦} of points in 𝑎 is related by 𝑣". Definition 2 of [BourbakiTop1] p. II.13. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ CauFilu = (𝑢 ∈ ∪ ran UnifOn ↦ {𝑓 ∈ (fBas‘dom ∪ 𝑢) ∣ ∀𝑣 ∈ 𝑢 ∃𝑎 ∈ 𝑓 (𝑎 × 𝑎) ⊆ 𝑣})
Theorem	iscfilu 24243*	The predicate "𝐹 is a Cauchy filter base on uniform space 𝑈". (Contributed by Thierry Arnoux, 18-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐹 ∈ (CauFilu‘𝑈) ↔ (𝐹 ∈ (fBas‘𝑋) ∧ ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ 𝐹 (𝑎 × 𝑎) ⊆ 𝑣)))
Theorem	cfilufbas 24244	A Cauchy filter base is a filter base. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐹 ∈ (CauFilu‘𝑈)) → 𝐹 ∈ (fBas‘𝑋))
Theorem	cfiluexsm 24245*	For a Cauchy filter base and any entourage 𝑉, there is an element of the filter small in 𝑉. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐹 ∈ (CauFilu‘𝑈) ∧ 𝑉 ∈ 𝑈) → ∃𝑎 ∈ 𝐹 (𝑎 × 𝑎) ⊆ 𝑉)
Theorem	fmucndlem 24246*	Lemma for fmucnd 24247. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝐴 × 𝐴)) = ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)))
Theorem	fmucnd 24247*	The image of a Cauchy filter base by an uniformly continuous function is a Cauchy filter base. Deduction form. Proposition 3 of [BourbakiTop1] p. II.13. (Contributed by Thierry Arnoux, 18-Nov-2017.)
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))    &   ⊢ (𝜑 → 𝐶 ∈ (CauFilu‘𝑈))    &   ⊢ 𝐷 = ran (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (CauFilu‘𝑉))
Theorem	cfilufg 24248	The filter generated by a Cauchy filter base is still a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐹 ∈ (CauFilu‘𝑈)) → (𝑋filGen𝐹) ∈ (CauFilu‘𝑈))
Theorem	trcfilu 24249	Condition for the trace of a Cauchy filter base to be a Cauchy filter base for the restricted uniform structure. (Contributed by Thierry Arnoux, 24-Jan-2018.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐹 ∈ (CauFilu‘𝑈) ∧ ¬ ∅ ∈ (𝐹 ↾t 𝐴)) ∧ 𝐴 ⊆ 𝑋) → (𝐹 ↾t 𝐴) ∈ (CauFilu‘(𝑈 ↾t (𝐴 × 𝐴))))
Theorem	cfiluweak 24250	A Cauchy filter base is also a Cauchy filter base on any coarser uniform structure. (Contributed by Thierry Arnoux, 24-Jan-2018.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ (CauFilu‘(𝑈 ↾t (𝐴 × 𝐴)))) → 𝐹 ∈ (CauFilu‘𝑈))
Theorem	neipcfilu 24251	In an uniform space, a neighboring filter is a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018.)
⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑈 = (UnifSt‘𝑊)    ⇒   ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) ∈ (CauFilu‘𝑈))
12.3.6  Complete uniform spaces
Syntax	ccusp 24252	Extend class notation with the class of all complete uniform spaces.
class CUnifSp
Definition	df-cusp 24253*	Define the class of all complete uniform spaces. Definition 3 of [BourbakiTop1] p. II.15. (Contributed by Thierry Arnoux, 1-Dec-2017.)
⊢ CUnifSp = {𝑤 ∈ UnifSp ∣ ∀𝑐 ∈ (Fil‘(Base‘𝑤))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)}
Theorem	iscusp 24254*	The predicate "𝑊 is a complete uniform space." (Contributed by Thierry Arnoux, 3-Dec-2017.)
⊢ (𝑊 ∈ CUnifSp ↔ (𝑊 ∈ UnifSp ∧ ∀𝑐 ∈ (Fil‘(Base‘𝑊))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑊)) → ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅)))
Theorem	cuspusp 24255	A complete uniform space is an uniform space. (Contributed by Thierry Arnoux, 3-Dec-2017.)
⊢ (𝑊 ∈ CUnifSp → 𝑊 ∈ UnifSp)
Theorem	cuspcvg 24256	In a complete uniform space, any Cauchy filter 𝐶 has a limit. (Contributed by Thierry Arnoux, 3-Dec-2017.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    ⇒   ⊢ ((𝑊 ∈ CUnifSp ∧ 𝐶 ∈ (CauFilu‘(UnifSt‘𝑊)) ∧ 𝐶 ∈ (Fil‘𝐵)) → (𝐽 fLim 𝐶) ≠ ∅)
Theorem	iscusp2 24257*	The predicate "𝑊 is a complete uniform space." (Contributed by Thierry Arnoux, 15-Dec-2017.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑈 = (UnifSt‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    ⇒   ⊢ (𝑊 ∈ CUnifSp ↔ (𝑊 ∈ UnifSp ∧ ∀𝑐 ∈ (Fil‘𝐵)(𝑐 ∈ (CauFilu‘𝑈) → (𝐽 fLim 𝑐) ≠ ∅)))
Theorem	cnextucn 24258*	Extension by continuity. Proposition 11 of [BourbakiTop1] p. II.20. Given a topology 𝐽 on 𝑋, a subset 𝐴 dense in 𝑋, this states a condition for 𝐹 from 𝐴 to a space 𝑌 Hausdorff and complete to be extensible by continuity. (Contributed by Thierry Arnoux, 4-Dec-2017.)
⊢ 𝑋 = (Base‘𝑉)    &   ⊢ 𝑌 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑉)    &   ⊢ 𝐾 = (TopOpen‘𝑊)    &   ⊢ 𝑈 = (UnifSt‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ TopSp)    &   ⊢ (𝜑 → 𝑊 ∈ TopSp)    &   ⊢ (𝜑 → 𝑊 ∈ CUnifSp)    &   ⊢ (𝜑 → 𝐾 ∈ Haus)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑌)    &   ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑌 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∈ (CauFilu‘𝑈))    ⇒   ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾))
Theorem	ucnextcn 24259	Extension by continuity. Theorem 2 of [BourbakiTop1] p. II.20. Given an uniform space on a set 𝑋, a subset 𝐴 dense in 𝑋, and a function 𝐹 uniformly continuous from 𝐴 to 𝑌, that function can be extended by continuity to the whole 𝑋, and its extension is uniformly continuous. (Contributed by Thierry Arnoux, 25-Jan-2018.)
⊢ 𝑋 = (Base‘𝑉)    &   ⊢ 𝑌 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑉)    &   ⊢ 𝐾 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (UnifSt‘𝑉)    &   ⊢ 𝑇 = (UnifSt‘(𝑉 ↾s 𝐴))    &   ⊢ 𝑈 = (UnifSt‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ TopSp)    &   ⊢ (𝜑 → 𝑉 ∈ UnifSp)    &   ⊢ (𝜑 → 𝑊 ∈ TopSp)    &   ⊢ (𝜑 → 𝑊 ∈ CUnifSp)    &   ⊢ (𝜑 → 𝐾 ∈ Haus)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑇 Cnu𝑈))    &   ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝑋)    ⇒   ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾))
12.4  Metric spaces
12.4.1  Pseudometric spaces
Theorem	ispsmet 24260*	Express the predicate "𝐷 is a pseudometric." (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ (𝑋 ∈ 𝑉 → (𝐷 ∈ (PsMet‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐷𝑥) = 0 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))))
Theorem	psmetdmdm 24261	Recover the base set from a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 = dom dom 𝐷)
Theorem	psmetf 24262	The distance function of a pseudometric as a function. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
Theorem	psmetcl 24263	Closure of the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ*)
Theorem	psmet0 24264	The distance function of a pseudometric space is zero if its arguments are equal. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 0)
Theorem	psmettri2 24265	Triangle inequality for the distance function of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵)))
Theorem	psmetsym 24266	The distance function of a pseudometric is symmetrical. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
Theorem	psmettri 24267	Triangle inequality for the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐶𝐷𝐵)))
Theorem	psmetge0 24268	The distance function of a pseudometric space is nonnegative. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵))
Theorem	psmetxrge0 24269	The distance function of a pseudometric space is a function into the nonnegative extended real numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.)
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞))
Theorem	psmetres2 24270	Restriction of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (PsMet‘𝑅))
Theorem	psmetlecl 24271	Real closure of an extended metric value that is upper bounded by a real. (Contributed by Thierry Arnoux, 11-Mar-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ ℝ ∧ (𝐴𝐷𝐵) ≤ 𝐶)) → (𝐴𝐷𝐵) ∈ ℝ)
Theorem	distspace 24272	A set 𝑋 together with a (distance) function 𝐷 which is a pseudometric is a distance space (according to E. Deza, M.M. Deza: "Dictionary of Distances", Elsevier, 2006), i.e. a (base) set 𝑋 equipped with a distance 𝐷, which is a mapping of two elements of the base set to the (extended) reals and which is nonnegative, symmetric and equal to 0 if the two elements are equal. (Contributed by AV, 15-Oct-2021.) (Revised by AV, 5-Jul-2022.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ (𝐴𝐷𝐴) = 0) ∧ (0 ≤ (𝐴𝐷𝐵) ∧ (𝐴𝐷𝐵) = (𝐵𝐷𝐴))))
12.4.2  Basic metric space properties
Syntax	cxms 24273	Extend class notation with the class of extended metric spaces.
class ∞MetSp
Syntax	cms 24274	Extend class notation with the class of metric spaces.
class MetSp
Syntax	ctms 24275	Extend class notation with the function mapping a metric to the metric space it defines.
class toMetSp
Definition	df-xms 24276	Define the (proper) class of extended metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ ∞MetSp = {𝑓 ∈ TopSp ∣ (TopOpen‘𝑓) = (MetOpen‘((dist‘𝑓) ↾ ((Base‘𝑓) × (Base‘𝑓))))}
Definition	df-ms 24277	Define the (proper) class of metric spaces. (Contributed by NM, 27-Aug-2006.)
⊢ MetSp = {𝑓 ∈ ∞MetSp ∣ ((dist‘𝑓) ↾ ((Base‘𝑓) × (Base‘𝑓))) ∈ (Met‘(Base‘𝑓))}
Definition	df-tms 24278	Define the function mapping a metric to the metric space which it defines. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ toMetSp = (𝑑 ∈ ∪ ran ∞Met ↦ ({⟨(Base‘ndx), dom dom 𝑑⟩, ⟨(dist‘ndx), 𝑑⟩} sSet ⟨(TopSet‘ndx), (MetOpen‘𝑑)⟩))
Theorem	ismet 24279*	Express the predicate "𝐷 is a metric." (Contributed by NM, 25-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ (𝑋 ∈ 𝐴 → (𝐷 ∈ (Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))))))
Theorem	isxmet 24280*	Express the predicate "𝐷 is an extended metric." (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝑋 ∈ 𝐴 → (𝐷 ∈ (∞Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))))
Theorem	ismeti 24281*	Properties that determine a metric. (Contributed by NM, 17-Nov-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ 𝑋 ∈ V    &   ⊢ 𝐷:(𝑋 × 𝑋)⟶ℝ    &   ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦))    &   ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))    ⇒   ⊢ 𝐷 ∈ (Met‘𝑋)
Theorem	isxmetd 24282*	Properties that determine an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) (Revised by AV, 9-Apr-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
Theorem	isxmet2d 24283*	It is safe to only require the triangle inequality when the values are real (so that we can use the standard addition over the reals), but in this case the nonnegativity constraint cannot be deduced and must be provided separately. (Counterexample: 𝐷(𝑥, 𝑦) = if(𝑥 = 𝑦, 0, -∞) satisfies all hypotheses except nonnegativity.) (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (𝑥𝐷𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
Theorem	metflem 24284*	Lemma for metf 24286 and others. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ (𝐷 ∈ (Met‘𝑋) → (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))))
Theorem	xmetf 24285	Mapping of the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
Theorem	metf 24286	Mapping of the distance function of a metric space. (Contributed by NM, 30-Aug-2006.)
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ)
Theorem	xmetcl 24287	Closure of the distance function of a metric space. Part of Property M1 of [Kreyszig] p. 3. (Contributed by NM, 30-Aug-2006.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ*)
Theorem	metcl 24288	Closure of the distance function of a metric space. Part of Property M1 of [Kreyszig] p. 3. (Contributed by NM, 30-Aug-2006.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ)
Theorem	ismet2 24289	An extended metric is a metric exactly when it takes real values for all values of the arguments. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐷 ∈ (Met‘𝑋) ↔ (𝐷 ∈ (∞Met‘𝑋) ∧ 𝐷:(𝑋 × 𝑋)⟶ℝ))
Theorem	metxmet 24290	A metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
Theorem	xmetdmdm 24291	Recover the base set from an extended metric. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = dom dom 𝐷)
Theorem	metdmdm 24292	Recover the base set from a metric. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (𝐷 ∈ (Met‘𝑋) → 𝑋 = dom dom 𝐷)
Theorem	xmetunirn 24293	Two ways to express an extended metric on an unspecified base. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ (𝐷 ∈ ∪ ran ∞Met ↔ 𝐷 ∈ (∞Met‘dom dom 𝐷))
Theorem	xmeteq0 24294	The value of an extended metric is zero iff its arguments are equal. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐷𝐵) = 0 ↔ 𝐴 = 𝐵))
Theorem	meteq0 24295	The value of a metric is zero iff its arguments are equal. Property M2 of [Kreyszig] p. 4. (Contributed by NM, 30-Aug-2006.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐷𝐵) = 0 ↔ 𝐴 = 𝐵))
Theorem	xmettri2 24296	Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵)))
Theorem	mettri2 24297	Triangle inequality for the distance function of a metric space. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) + (𝐶𝐷𝐵)))
Theorem	xmet0 24298	The distance function of a metric space is zero if its arguments are equal. Definition 14-1.1(a) of [Gleason] p. 223. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 0)
Theorem	met0 24299	The distance function of a metric space is zero if its arguments are equal. Definition 14-1.1(a) of [Gleason] p. 223. (Contributed by NM, 30-Aug-2006.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 0)
Theorem	xmetge0 24300	The distance function of a metric space is nonnegative. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵))