![]() |
Metamath
Proof Explorer Theorem List (p. 353 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cnres2 35201* | The restriction of a continuous function to a subset is continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐹 ∈ (𝐽 Cn 𝐾) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn (𝐾 ↾t 𝐵))) | ||
Theorem | cnresima 35202 | A continuous function is continuous onto its image. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (𝐽 Cn (𝐾 ↾t ran 𝐹))) | ||
Theorem | cncfres 35203* | A continuous function on complex numbers restricted to a subset. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐴 ⊆ ℂ & ⊢ 𝐵 ⊆ ℂ & ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝐶) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵) & ⊢ 𝐹 ∈ (ℂ–cn→ℂ) & ⊢ 𝐽 = (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))) & ⊢ 𝐾 = (MetOpen‘((abs ∘ − ) ↾ (𝐵 × 𝐵))) ⇒ ⊢ 𝐺 ∈ (𝐽 Cn 𝐾) | ||
Syntax | ctotbnd 35204 | Extend class notation with the class of totally bounded metric spaces. |
class TotBnd | ||
Syntax | cbnd 35205 | Extend class notation with the class of bounded metric spaces. |
class Bnd | ||
Definition | df-totbnd 35206* | Define the class of totally bounded metrics. A metric space is totally bounded iff it can be covered by a finite number of balls of any given radius. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ TotBnd = (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑥 ∧ ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))}) | ||
Theorem | istotbnd 35207* | The predicate "is a totally bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑋 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) | ||
Theorem | istotbnd2 35208* | The predicate "is a totally bounded metric space." (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑀 ∈ (Met‘𝑋) → (𝑀 ∈ (TotBnd‘𝑋) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑋 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) | ||
Theorem | istotbnd3 35209* | A metric space is totally bounded iff there is a finite ε-net for every positive ε. This differs from the definition in providing a finite set of ball centers rather than a finite set of balls. (Contributed by Mario Carneiro, 12-Sep-2015.) |
⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) | ||
Theorem | totbndmet 35210 | The predicate "totally bounded" implies 𝑀 is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑀 ∈ (TotBnd‘𝑋) → 𝑀 ∈ (Met‘𝑋)) | ||
Theorem | 0totbnd 35211 | The metric (there is only one) on the empty set is totally bounded. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ (𝑋 = ∅ → (𝑀 ∈ (TotBnd‘𝑋) ↔ 𝑀 ∈ (Met‘𝑋))) | ||
Theorem | sstotbnd2 35212* | Condition for a subset of a metric space to be totally bounded. (Contributed by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))) | ||
Theorem | sstotbnd 35213* | Condition for a subset of a metric space to be totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) | ||
Theorem | sstotbnd3 35214* | Use a net that is not necessarily finite, but for which only finitely many balls meet the subset. (Contributed by Mario Carneiro, 14-Sep-2015.) |
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ 𝒫 𝑋(𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) ∧ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌) ≠ ∅} ∈ Fin))) | ||
Theorem | totbndss 35215 | A subset of a totally bounded metric space is totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ ((𝑀 ∈ (TotBnd‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑀 ↾ (𝑆 × 𝑆)) ∈ (TotBnd‘𝑆)) | ||
Theorem | equivtotbnd 35216* | If the metric 𝑀 is "strongly finer" than 𝑁 (meaning that there is a positive real constant 𝑅 such that 𝑁(𝑥, 𝑦) ≤ 𝑅 · 𝑀(𝑥, 𝑦)), then total boundedness of 𝑀 implies total boundedness of 𝑁. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then one is totally bounded iff the other is.) (Contributed by Mario Carneiro, 14-Sep-2015.) |
⊢ (𝜑 → 𝑀 ∈ (TotBnd‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑁𝑦) ≤ (𝑅 · (𝑥𝑀𝑦))) ⇒ ⊢ (𝜑 → 𝑁 ∈ (TotBnd‘𝑋)) | ||
Definition | df-bnd 35217* | Define the class of bounded metrics. A metric space is bounded iff it can be covered by a single ball. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ Bnd = (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑥 = (𝑦(ball‘𝑚)𝑟)}) | ||
Theorem | isbnd 35218* | The predicate "is a bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟))) | ||
Theorem | bndmet 35219 | A bounded metric space is a metric space. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ (𝑀 ∈ (Bnd‘𝑋) → 𝑀 ∈ (Met‘𝑋)) | ||
Theorem | isbndx 35220* | A "bounded extended metric" (meaning that it satisfies the same condition as a bounded metric, but with "metric" replaced with "extended metric") is a metric and thus is bounded in the conventional sense. (Contributed by Mario Carneiro, 12-Sep-2015.) |
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (∞Met‘𝑋) ∧ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟))) | ||
Theorem | isbnd2 35221* | The predicate "is a bounded metric space". Uses a single point instead of an arbitrary point in the space. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) ↔ (𝑀 ∈ (∞Met‘𝑋) ∧ ∃𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟))) | ||
Theorem | isbnd3 35222* | A metric space is bounded iff the metric function maps to some bounded real interval. (Contributed by Mario Carneiro, 13-Sep-2015.) |
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))) | ||
Theorem | isbnd3b 35223* | A metric space is bounded iff the metric function maps to some bounded real interval. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦𝑀𝑧) ≤ 𝑥)) | ||
Theorem | bndss 35224 | A subset of a bounded metric space is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑀 ↾ (𝑆 × 𝑆)) ∈ (Bnd‘𝑆)) | ||
Theorem | blbnd 35225 | A ball is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 15-Jan-2014.) |
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ) → (𝑀 ↾ ((𝑌(ball‘𝑀)𝑅) × (𝑌(ball‘𝑀)𝑅))) ∈ (Bnd‘(𝑌(ball‘𝑀)𝑅))) | ||
Theorem | ssbnd 35226* | A subset of a metric space is bounded iff it is contained in a ball around 𝑃, for any 𝑃 in the larger space. (Contributed by Mario Carneiro, 14-Sep-2015.) |
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ (Bnd‘𝑌) ↔ ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) | ||
Theorem | totbndbnd 35227 | A totally bounded metric space is bounded. This theorem fails for extended metrics - a bounded extended metric is a metric, but there are totally bounded extended metrics that are not metrics (if we were to weaken istotbnd 35207 to only require that 𝑀 be an extended metric). A counterexample is the discrete extended metric (assigning distinct points distance +∞) on a finite set. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
⊢ (𝑀 ∈ (TotBnd‘𝑋) → 𝑀 ∈ (Bnd‘𝑋)) | ||
Theorem | equivbnd 35228* | If the metric 𝑀 is "strongly finer" than 𝑁 (meaning that there is a positive real constant 𝑅 such that 𝑁(𝑥, 𝑦) ≤ 𝑅 · 𝑀(𝑥, 𝑦)), then boundedness of 𝑀 implies boundedness of 𝑁. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then one is bounded iff the other is.) (Contributed by Mario Carneiro, 14-Sep-2015.) |
⊢ (𝜑 → 𝑀 ∈ (Bnd‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑁𝑦) ≤ (𝑅 · (𝑥𝑀𝑦))) ⇒ ⊢ (𝜑 → 𝑁 ∈ (Bnd‘𝑋)) | ||
Theorem | bnd2lem 35229 | Lemma for equivbnd2 35230 and similar theorems. (Contributed by Jeff Madsen, 16-Sep-2015.) |
⊢ 𝐷 = (𝑀 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝐷 ∈ (Bnd‘𝑌)) → 𝑌 ⊆ 𝑋) | ||
Theorem | equivbnd2 35230* | If balls are totally bounded in the metric 𝑀, then balls are totally bounded in the equivalent metric 𝑁. (Contributed by Mario Carneiro, 15-Sep-2015.) |
⊢ (𝜑 → 𝑀 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝑆 ∈ ℝ+) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑁𝑦) ≤ (𝑅 · (𝑥𝑀𝑦))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑀𝑦) ≤ (𝑆 · (𝑥𝑁𝑦))) & ⊢ 𝐶 = (𝑀 ↾ (𝑌 × 𝑌)) & ⊢ 𝐷 = (𝑁 ↾ (𝑌 × 𝑌)) & ⊢ (𝜑 → (𝐶 ∈ (TotBnd‘𝑌) ↔ 𝐶 ∈ (Bnd‘𝑌))) ⇒ ⊢ (𝜑 → (𝐷 ∈ (TotBnd‘𝑌) ↔ 𝐷 ∈ (Bnd‘𝑌))) | ||
Theorem | prdsbnd 35231* | The product metric over finite index set is bounded if all the factors are bounded. (Contributed by Mario Carneiro, 13-Sep-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑉 = (Base‘(𝑅‘𝑥)) & ⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Bnd‘𝑉)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (Bnd‘𝐵)) | ||
Theorem | prdstotbnd 35232* | The product metric over finite index set is totally bounded if all the factors are totally bounded. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑉 = (Base‘(𝑅‘𝑥)) & ⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (TotBnd‘𝑉)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (TotBnd‘𝐵)) | ||
Theorem | prdsbnd2 35233* | If balls are totally bounded in each factor, then balls are bounded in a metric product. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑉 = (Base‘(𝑅‘𝑥)) & ⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ 𝐶 = (𝐷 ↾ (𝐴 × 𝐴)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦))) ⇒ ⊢ (𝜑 → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Bnd‘𝐴))) | ||
Theorem | cntotbnd 35234 | A subset of the complex numbers is totally bounded iff it is bounded. (Contributed by Mario Carneiro, 14-Sep-2015.) |
⊢ 𝐷 = ((abs ∘ − ) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝐷 ∈ (TotBnd‘𝑋) ↔ 𝐷 ∈ (Bnd‘𝑋)) | ||
Theorem | cnpwstotbnd 35235 | A subset of 𝐴↑𝐼, where 𝐴 ⊆ ℂ, is totally bounded iff it is bounded. (Contributed by Mario Carneiro, 14-Sep-2015.) |
⊢ 𝑌 = ((ℂfld ↾s 𝐴) ↑s 𝐼) & ⊢ 𝐷 = ((dist‘𝑌) ↾ (𝑋 × 𝑋)) ⇒ ⊢ ((𝐴 ⊆ ℂ ∧ 𝐼 ∈ Fin) → (𝐷 ∈ (TotBnd‘𝑋) ↔ 𝐷 ∈ (Bnd‘𝑋))) | ||
Syntax | cismty 35236 | Extend class notation with the class of metric space isometries. |
class Ismty | ||
Definition | df-ismty 35237* | Define a function which takes two metric spaces and returns the set of isometries between the spaces. An isometry is a bijection which preserves distance. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ Ismty = (𝑚 ∈ ∪ ran ∞Met, 𝑛 ∈ ∪ ran ∞Met ↦ {𝑓 ∣ (𝑓:dom dom 𝑚–1-1-onto→dom dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)))}) | ||
Theorem | ismtyval 35238* | The set of isometries between two metric spaces. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝑀 Ismty 𝑁) = {𝑓 ∣ (𝑓:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦)))}) | ||
Theorem | isismty 35239* | The condition "is an isometry". (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝐹 ∈ (𝑀 Ismty 𝑁) ↔ (𝐹:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝐹‘𝑥)𝑁(𝐹‘𝑦))))) | ||
Theorem | ismtycnv 35240 | The inverse of an isometry is an isometry. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝐹 ∈ (𝑀 Ismty 𝑁) → ◡𝐹 ∈ (𝑁 Ismty 𝑀))) | ||
Theorem | ismtyima 35241 | The image of a ball under an isometry is another ball. (Contributed by Jeff Madsen, 31-Jan-2014.) |
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝑀 Ismty 𝑁)) ∧ (𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*)) → (𝐹 “ (𝑃(ball‘𝑀)𝑅)) = ((𝐹‘𝑃)(ball‘𝑁)𝑅)) | ||
Theorem | ismtyhmeolem 35242 | Lemma for ismtyhmeo 35243. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐽 = (MetOpen‘𝑀) & ⊢ 𝐾 = (MetOpen‘𝑁) & ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) & ⊢ (𝜑 → 𝐹 ∈ (𝑀 Ismty 𝑁)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) | ||
Theorem | ismtyhmeo 35243 | An isometry is a homeomorphism on the induced topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐽 = (MetOpen‘𝑀) & ⊢ 𝐾 = (MetOpen‘𝑁) ⇒ ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝑀 Ismty 𝑁) ⊆ (𝐽Homeo𝐾)) | ||
Theorem | ismtybndlem 35244 | Lemma for ismtybnd 35245. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 19-Jan-2014.) |
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝑀 Ismty 𝑁)) → (𝑀 ∈ (Bnd‘𝑋) → 𝑁 ∈ (Bnd‘𝑌))) | ||
Theorem | ismtybnd 35245 | Isometries preserve boundedness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 19-Jan-2014.) |
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝑀 Ismty 𝑁)) → (𝑀 ∈ (Bnd‘𝑋) ↔ 𝑁 ∈ (Bnd‘𝑌))) | ||
Theorem | ismtyres 35246 | A restriction of an isometry is an isometry. The condition 𝐴 ⊆ 𝑋 is not necessary but makes the proof easier. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐵 = (𝐹 “ 𝐴) & ⊢ 𝑆 = (𝑀 ↾ (𝐴 × 𝐴)) & ⊢ 𝑇 = (𝑁 ↾ (𝐵 × 𝐵)) ⇒ ⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ (𝑀 Ismty 𝑁) ∧ 𝐴 ⊆ 𝑋)) → (𝐹 ↾ 𝐴) ∈ (𝑆 Ismty 𝑇)) | ||
Theorem | heibor1lem 35247 | Lemma for heibor1 35248. A compact metric space is complete. This proof works by considering the collection cls(𝐹 “ (ℤ≥‘𝑛)) for each 𝑛 ∈ ℕ, which has the finite intersection property because any finite intersection of upper integer sets is another upper integer set, so any finite intersection of the image closures will contain (𝐹 “ (ℤ≥‘𝑚)) for some 𝑚. Thus, by compactness, the intersection contains a point 𝑦, which must then be the convergent point of 𝐹. (Contributed by Jeff Madsen, 17-Jan-2014.) (Revised by Mario Carneiro, 5-Jun-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐽 ∈ Comp) & ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷)) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑋) ⇒ ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽)) | ||
Theorem | heibor1 35248 | One half of heibor 35259, that does not require any Choice. A compact metric space is complete and totally bounded. We prove completeness in cmpcmet 23923 and total boundedness here, which follows trivially from the fact that the set of all 𝑟-balls is an open cover of 𝑋, so finitely many cover 𝑋. (Contributed by Jeff Madsen, 16-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp) → (𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋))) | ||
Theorem | heiborlem1 35249* | Lemma for heibor 35259. We work with a fixed open cover 𝑈 throughout. The set 𝐾 is the set of all subsets of 𝑋 that admit no finite subcover of 𝑈. (We wish to prove that 𝐾 is empty.) If a set 𝐶 has no finite subcover, then any finite cover of 𝐶 must contain a set that also has no finite subcover. (Contributed by Jeff Madsen, 23-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐾) → ∃𝑥 ∈ 𝐴 𝐵 ∈ 𝐾) | ||
Theorem | heiborlem2 35250* | Lemma for heibor 35259. Substitutions for the set 𝐺. (Contributed by Jeff Madsen, 23-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐴 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴𝐺𝐶 ↔ (𝐶 ∈ ℕ0 ∧ 𝐴 ∈ (𝐹‘𝐶) ∧ (𝐴𝐵𝐶) ∈ 𝐾)) | ||
Theorem | heiborlem3 35251* | Lemma for heibor 35259. Using countable choice ax-cc 9846, we have fixed in advance a collection of finite 2↑-𝑛 nets (𝐹‘𝑛) for 𝑋 (note that an 𝑟-net is a set of points in 𝑋 whose 𝑟 -balls cover 𝑋). The set 𝐺 is the subset of these points whose corresponding balls have no finite subcover (i.e. in the set 𝐾). If the theorem was false, then 𝑋 would be in 𝐾, and so some ball at each level would also be in 𝐾. But we can say more than this; given a ball (𝑦𝐵𝑛) on level 𝑛, since level 𝑛 + 1 covers the space and thus also (𝑦𝐵𝑛), using heiborlem1 35249 there is a ball on the next level whose intersection with (𝑦𝐵𝑛) also has no finite subcover. Now since the set 𝐺 is a countable union of finite sets, it is countable (which needs ax-cc 9846 via iunctb 9985), and so we can apply ax-cc 9846 to 𝐺 directly to get a function from 𝐺 to itself, which points from each ball in 𝐾 to a ball on the next level in 𝐾, and such that the intersection between these balls is also in 𝐾. (Contributed by Jeff Madsen, 18-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) ⇒ ⊢ (𝜑 → ∃𝑔∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) | ||
Theorem | heiborlem4 35252* | Lemma for heibor 35259. Using the function 𝑇 constructed in heiborlem3 35251, construct an infinite path in 𝐺. (Contributed by Jeff Madsen, 23-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) & ⊢ (𝜑 → 𝐶𝐺0) & ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ0) → (𝑆‘𝐴)𝐺𝐴) | ||
Theorem | heiborlem5 35253* | Lemma for heibor 35259. The function 𝑀 is a set of point-and-radius pairs suitable for application to caubl 23912. (Contributed by Jeff Madsen, 23-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) & ⊢ (𝜑 → 𝐶𝐺0) & ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))) & ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ 〈(𝑆‘𝑛), (3 / (2↑𝑛))〉) ⇒ ⊢ (𝜑 → 𝑀:ℕ⟶(𝑋 × ℝ+)) | ||
Theorem | heiborlem6 35254* | Lemma for heibor 35259. Since the sequence of balls connected by the function 𝑇 ensures that each ball nontrivially intersects with the next (since the empty set has a finite subcover, the intersection of any two successive balls in the sequence is nonempty), and each ball is half the size of the previous one, the distance between the centers is at most 3 / 2 times the size of the larger, and so if we expand each ball by a factor of 3 we get a nested sequence of balls. (Contributed by Jeff Madsen, 23-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) & ⊢ (𝜑 → 𝐶𝐺0) & ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))) & ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ 〈(𝑆‘𝑛), (3 / (2↑𝑛))〉) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ ℕ ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀‘𝑘))) | ||
Theorem | heiborlem7 35255* | Lemma for heibor 35259. Since the sizes of the balls decrease exponentially, the sequence converges to zero. (Contributed by Jeff Madsen, 23-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) & ⊢ (𝜑 → 𝐶𝐺0) & ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))) & ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ 〈(𝑆‘𝑛), (3 / (2↑𝑛))〉) ⇒ ⊢ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ (2nd ‘(𝑀‘𝑘)) < 𝑟 | ||
Theorem | heiborlem8 35256* | Lemma for heibor 35259. The previous lemmas establish that the sequence 𝑀 is Cauchy, so using completeness we now consider the convergent point 𝑌. By assumption, 𝑈 is an open cover, so 𝑌 is an element of some 𝑍 ∈ 𝑈, and some ball centered at 𝑌 is contained in 𝑍. But the sequence contains arbitrarily small balls close to 𝑌, so some element ball(𝑀‘𝑛) of the sequence is contained in 𝑍. And finally we arrive at a contradiction, because {𝑍} is a finite subcover of 𝑈 that covers ball(𝑀‘𝑛), yet ball(𝑀‘𝑛) ∈ 𝐾. For convenience, we write this contradiction as 𝜑 → 𝜓 where 𝜑 is all the accumulated hypotheses and 𝜓 is anything at all. (Contributed by Jeff Madsen, 22-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) & ⊢ (𝜑 → 𝐶𝐺0) & ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))) & ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ 〈(𝑆‘𝑛), (3 / (2↑𝑛))〉) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ 𝑌 ∈ V & ⊢ (𝜑 → 𝑌 ∈ 𝑍) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → (1st ∘ 𝑀)(⇝𝑡‘𝐽)𝑌) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | heiborlem9 35257* | Lemma for heibor 35259. Discharge the hypotheses of heiborlem8 35256 by applying caubl 23912 to get a convergent point and adding the open cover assumption. (Contributed by Jeff Madsen, 20-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) & ⊢ (𝜑 → 𝐶𝐺0) & ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))) & ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ 〈(𝑆‘𝑛), (3 / (2↑𝑛))〉) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → ∪ 𝑈 = 𝑋) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | heiborlem10 35258* | Lemma for heibor 35259. The last remaining piece of the proof is to find an element 𝐶 such that 𝐶𝐺0, i.e. 𝐶 is an element of (𝐹‘0) that has no finite subcover, which is true by heiborlem1 35249, since (𝐹‘0) is a finite cover of 𝑋, which has no finite subcover. Thus, the rest of the proof follows to a contradiction, and thus there must be a finite subcover of 𝑈 that covers 𝑋, i.e. 𝑋 is compact. (Contributed by Jeff Madsen, 22-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) ⇒ ⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈)) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∪ 𝐽 = ∪ 𝑣) | ||
Theorem | heibor 35259 | Generalized Heine-Borel Theorem. A metric space is compact iff it is complete and totally bounded. See heibor1 35248 and heiborlem1 35249 for a description of the proof. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp) ↔ (𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋))) | ||
Theorem | bfplem1 35260* | Lemma for bfp 35262. The sequence 𝐺, which simply starts from any point in the space and iterates 𝐹, satisfies the property that the distance from 𝐺(𝑛) to 𝐺(𝑛 + 1) decreases by at least 𝐾 after each step. Thus, the total distance from any 𝐺(𝑖) to 𝐺(𝑗) is bounded by a geometric series, and the sequence is Cauchy. Therefore, it converges to a point ((⇝𝑡‘𝐽)‘𝐺) since the space is complete. (Contributed by Jeff Madsen, 17-Jun-2014.) |
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐾 ∈ ℝ+) & ⊢ (𝜑 → 𝐾 < 1) & ⊢ (𝜑 → 𝐹:𝑋⟶𝑋) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦))) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐺 = seq1((𝐹 ∘ 1st ), (ℕ × {𝐴})) ⇒ ⊢ (𝜑 → 𝐺(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐺)) | ||
Theorem | bfplem2 35261* | Lemma for bfp 35262. Using the point found in bfplem1 35260, we show that this convergent point is a fixed point of 𝐹. Since for any positive 𝑥, the sequence 𝐺 is in 𝐵(𝑥 / 2, 𝑃) for all 𝑘 ∈ (ℤ≥‘𝑗) (where 𝑃 = ((⇝𝑡‘𝐽)‘𝐺)), we have 𝐷(𝐺(𝑗 + 1), 𝐹(𝑃)) ≤ 𝐷(𝐺(𝑗), 𝑃) < 𝑥 / 2 and 𝐷(𝐺(𝑗 + 1), 𝑃) < 𝑥 / 2, so 𝐹(𝑃) is in every neighborhood of 𝑃 and 𝑃 is a fixed point of 𝐹. (Contributed by Jeff Madsen, 5-Jun-2014.) |
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐾 ∈ ℝ+) & ⊢ (𝜑 → 𝐾 < 1) & ⊢ (𝜑 → 𝐹:𝑋⟶𝑋) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦))) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐺 = seq1((𝐹 ∘ 1st ), (ℕ × {𝐴})) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑧) | ||
Theorem | bfp 35262* | Banach fixed point theorem, also known as contraction mapping theorem. A contraction on a complete metric space has a unique fixed point. We show existence in the lemmas, and uniqueness here - if 𝐹 has two fixed points, then the distance between them is less than 𝐾 times itself, a contradiction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) |
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐾 ∈ ℝ+) & ⊢ (𝜑 → 𝐾 < 1) & ⊢ (𝜑 → 𝐹:𝑋⟶𝑋) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦))) ⇒ ⊢ (𝜑 → ∃!𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑧) | ||
Syntax | crrn 35263 | Extend class notation with the n-dimensional Euclidean space. |
class ℝn | ||
Definition | df-rrn 35264* | Define n-dimensional Euclidean space as a metric space with the standard Euclidean norm given by the quadratic mean. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ℝn = (𝑖 ∈ Fin ↦ (𝑥 ∈ (ℝ ↑m 𝑖), 𝑦 ∈ (ℝ ↑m 𝑖) ↦ (√‘Σ𝑘 ∈ 𝑖 (((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))) | ||
Theorem | rrnval 35265* | The n-dimensional Euclidean space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) |
⊢ 𝑋 = (ℝ ↑m 𝐼) ⇒ ⊢ (𝐼 ∈ Fin → (ℝn‘𝐼) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))) | ||
Theorem | rrnmval 35266* | The value of the Euclidean metric. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) |
⊢ 𝑋 = (ℝ ↑m 𝐼) ⇒ ⊢ ((𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹(ℝn‘𝐼)𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))) | ||
Theorem | rrnmet 35267 | Euclidean space is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) |
⊢ 𝑋 = (ℝ ↑m 𝐼) ⇒ ⊢ (𝐼 ∈ Fin → (ℝn‘𝐼) ∈ (Met‘𝑋)) | ||
Theorem | rrndstprj1 35268 | The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) |
⊢ 𝑋 = (ℝ ↑m 𝐼) & ⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ (((𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼) ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹‘𝐴)𝑀(𝐺‘𝐴)) ≤ (𝐹(ℝn‘𝐼)𝐺)) | ||
Theorem | rrndstprj2 35269* | Bound on the distance between two points in Euclidean space given bounds on the distances in each coordinate. This theorem and rrndstprj1 35268 can be used to show that the supremum norm and Euclidean norm are equivalent. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) |
⊢ 𝑋 = (ℝ ↑m 𝐼) & ⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝐹(ℝn‘𝐼)𝐺) < (𝑅 · (√‘(♯‘𝐼)))) | ||
Theorem | rrncmslem 35270* | Lemma for rrncms 35271. (Contributed by Jeff Madsen, 6-Jun-2014.) (Revised by Mario Carneiro, 13-Sep-2015.) |
⊢ 𝑋 = (ℝ ↑m 𝐼) & ⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝐽 = (MetOpen‘(ℝn‘𝐼)) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐹 ∈ (Cau‘(ℝn‘𝐼))) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑋) & ⊢ 𝑃 = (𝑚 ∈ 𝐼 ↦ ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑚)))) ⇒ ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽)) | ||
Theorem | rrncms 35271 | Euclidean space is complete. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) |
⊢ 𝑋 = (ℝ ↑m 𝐼) ⇒ ⊢ (𝐼 ∈ Fin → (ℝn‘𝐼) ∈ (CMet‘𝑋)) | ||
Theorem | repwsmet 35272 | The supremum metric on ℝ↑𝐼 is a metric. (Contributed by Jeff Madsen, 15-Sep-2015.) |
⊢ 𝑌 = ((ℂfld ↾s ℝ) ↑s 𝐼) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ 𝑋 = (ℝ ↑m 𝐼) ⇒ ⊢ (𝐼 ∈ Fin → 𝐷 ∈ (Met‘𝑋)) | ||
Theorem | rrnequiv 35273 | The supremum metric on ℝ↑𝐼 is equivalent to the ℝn metric. (Contributed by Jeff Madsen, 15-Sep-2015.) |
⊢ 𝑌 = ((ℂfld ↾s ℝ) ↑s 𝐼) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ 𝑋 = (ℝ ↑m 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) ⇒ ⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹𝐷𝐺) ≤ (𝐹(ℝn‘𝐼)𝐺) ∧ (𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)))) | ||
Theorem | rrntotbnd 35274 | A set in Euclidean space is totally bounded iff its is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 16-Sep-2015.) |
⊢ 𝑋 = (ℝ ↑m 𝐼) & ⊢ 𝑀 = ((ℝn‘𝐼) ↾ (𝑌 × 𝑌)) ⇒ ⊢ (𝐼 ∈ Fin → (𝑀 ∈ (TotBnd‘𝑌) ↔ 𝑀 ∈ (Bnd‘𝑌))) | ||
Theorem | rrnheibor 35275 | Heine-Borel theorem for Euclidean space. A subset of Euclidean space is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝑋 = (ℝ ↑m 𝐼) & ⊢ 𝑀 = ((ℝn‘𝐼) ↾ (𝑌 × 𝑌)) & ⊢ 𝑇 = (MetOpen‘𝑀) & ⊢ 𝑈 = (MetOpen‘(ℝn‘𝐼)) ⇒ ⊢ ((𝐼 ∈ Fin ∧ 𝑌 ⊆ 𝑋) → (𝑇 ∈ Comp ↔ (𝑌 ∈ (Clsd‘𝑈) ∧ 𝑀 ∈ (Bnd‘𝑌)))) | ||
Theorem | ismrer1 35276* | An isometry between ℝ and ℝ↑1. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝑅 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ({𝐴} × {𝑥})) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹 ∈ (𝑅 Ismty (ℝn‘{𝐴}))) | ||
Theorem | reheibor 35277 | Heine-Borel theorem for real numbers. A subset of ℝ is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝑀 = ((abs ∘ − ) ↾ (𝑌 × 𝑌)) & ⊢ 𝑇 = (MetOpen‘𝑀) & ⊢ 𝑈 = (topGen‘ran (,)) ⇒ ⊢ (𝑌 ⊆ ℝ → (𝑇 ∈ Comp ↔ (𝑌 ∈ (Clsd‘𝑈) ∧ 𝑀 ∈ (Bnd‘𝑌)))) | ||
Theorem | iccbnd 35278 | A closed interval in ℝ is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝐽 = (𝐴[,]𝐵) & ⊢ 𝑀 = ((abs ∘ − ) ↾ (𝐽 × 𝐽)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑀 ∈ (Bnd‘𝐽)) | ||
Theorem | icccmpALT 35279 | A closed interval in ℝ is compact. Alternate proof of icccmp 23430 using the Heine-Borel theorem heibor 35259. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Aug-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐽 = (𝐴[,]𝐵) & ⊢ 𝑀 = ((abs ∘ − ) ↾ (𝐽 × 𝐽)) & ⊢ 𝑇 = (MetOpen‘𝑀) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑇 ∈ Comp) | ||
Syntax | cass 35280 | Extend class notation with a device to add associativity to internal operations. |
class Ass | ||
Definition | df-ass 35281* | A device to add associativity to various sorts of internal operations. The definition is meaningful when 𝑔 is a magma at least. (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.) |
⊢ Ass = {𝑔 ∣ ∀𝑥 ∈ dom dom 𝑔∀𝑦 ∈ dom dom 𝑔∀𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))} | ||
Syntax | cexid 35282 | Extend class notation with the class of all the internal operations with an identity element. |
class ExId | ||
Definition | df-exid 35283* | A device to add an identity element to various sorts of internal operations. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
⊢ ExId = {𝑔 ∣ ∃𝑥 ∈ dom dom 𝑔∀𝑦 ∈ dom dom 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)} | ||
Theorem | isass 35284* | The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.) |
⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ Ass ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))) | ||
Theorem | isexid 35285* | The predicate 𝐺 has a left and right identity element. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ ExId ↔ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦))) | ||
Syntax | cmagm 35286 | Extend class notation with the class of all magmas. |
class Magma | ||
Definition | df-mgmOLD 35287* | Obsolete version of df-mgm 17844 as of 3-Feb-2020. A magma is a binary internal operation. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
⊢ Magma = {𝑔 ∣ ∃𝑡 𝑔:(𝑡 × 𝑡)⟶𝑡} | ||
Theorem | ismgmOLD 35288 | Obsolete version of ismgm 17845 as of 3-Feb-2020. The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ Magma ↔ 𝐺:(𝑋 × 𝑋)⟶𝑋)) | ||
Theorem | clmgmOLD 35289 | Obsolete version of mgmcl 17847 as of 3-Feb-2020. Closure of a magma. (Contributed by FL, 14-Sep-2010.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ ((𝐺 ∈ Magma ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋) | ||
Theorem | opidonOLD 35290 | Obsolete version of mndpfo 17926 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ (𝐺 ∈ (Magma ∩ ExId ) → 𝐺:(𝑋 × 𝑋)–onto→𝑋) | ||
Theorem | rngopidOLD 35291 | Obsolete version of mndpfo 17926 as of 23-Jan-2020. Range of an operation with a left and right identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐺 ∈ (Magma ∩ ExId ) → ran 𝐺 = dom dom 𝐺) | ||
Theorem | opidon2OLD 35292 | Obsolete version of mndpfo 17926 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ (Magma ∩ ExId ) → 𝐺:(𝑋 × 𝑋)–onto→𝑋) | ||
Theorem | isexid2 35293* | If 𝐺 ∈ (Magma ∩ ExId ), then it has a left and right identity element that belongs to the range of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ (Magma ∩ ExId ) → ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)) | ||
Theorem | exidu1 35294* | Uniqueness of the left and right identity element of a magma when it exists. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ (Magma ∩ ExId ) → ∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)) | ||
Theorem | idrval 35295* | The value of the identity element. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝐴 → 𝑈 = (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥))) | ||
Theorem | iorlid 35296 | A magma right and left identity belongs to the underlying set of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ (𝐺 ∈ (Magma ∩ ExId ) → 𝑈 ∈ 𝑋) | ||
Theorem | cmpidelt 35297 | A magma right and left identity element keeps the other elements unchanged. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝐴 ∈ 𝑋) → ((𝑈𝐺𝐴) = 𝐴 ∧ (𝐴𝐺𝑈) = 𝐴)) | ||
Syntax | csem 35298 | Extend class notation with the class of all semigroups. |
class SemiGrp | ||
Definition | df-sgrOLD 35299 | Obsolete version of df-sgrp 17893 as of 3-Feb-2020. A semigroup is an associative magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
⊢ SemiGrp = (Magma ∩ Ass) | ||
Theorem | smgrpismgmOLD 35300 | Obsolete version of sgrpmgm 17898 as of 3-Feb-2020. A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐺 ∈ SemiGrp → 𝐺 ∈ Magma) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |