![]() |
Metamath
Proof Explorer Theorem List (p. 314 of 429) | < 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-27903) |
![]() (27904-29428) |
![]() (29429-42879) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | erdszelem3 31301* | Lemma for erdsze 31310. (Contributed by Mario Carneiro, 22-Jan-2015.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ) & ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((# “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < )) ⇒ ⊢ (𝐴 ∈ (1...𝑁) → (𝐾‘𝐴) = sup((# “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}), ℝ, < )) | ||
Theorem | erdszelem4 31302* | Lemma for erdsze 31310. (Contributed by Mario Carneiro, 22-Jan-2015.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ) & ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((# “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < )) & ⊢ 𝑂 Or ℝ ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → {𝐴} ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}) | ||
Theorem | erdszelem5 31303* | Lemma for erdsze 31310. (Contributed by Mario Carneiro, 22-Jan-2015.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ) & ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((# “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < )) & ⊢ 𝑂 Or ℝ ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → (𝐾‘𝐴) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)})) | ||
Theorem | erdszelem6 31304* | Lemma for erdsze 31310. (Contributed by Mario Carneiro, 22-Jan-2015.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ) & ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((# “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < )) & ⊢ 𝑂 Or ℝ ⇒ ⊢ (𝜑 → 𝐾:(1...𝑁)⟶ℕ) | ||
Theorem | erdszelem7 31305* | Lemma for erdsze 31310. (Contributed by Mario Carneiro, 22-Jan-2015.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ) & ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((# “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < )) & ⊢ 𝑂 Or ℝ & ⊢ (𝜑 → 𝐴 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → ¬ (𝐾‘𝐴) ∈ (1...(𝑅 − 1))) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 (1...𝑁)(𝑅 ≤ (#‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠)))) | ||
Theorem | erdszelem8 31306* | Lemma for erdsze 31310. (Contributed by Mario Carneiro, 22-Jan-2015.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ) & ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((# “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < )) & ⊢ 𝑂 Or ℝ & ⊢ (𝜑 → 𝐴 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → ((𝐾‘𝐴) = (𝐾‘𝐵) → ¬ (𝐹‘𝐴)𝑂(𝐹‘𝐵))) | ||
Theorem | erdszelem9 31307* | Lemma for erdsze 31310. (Contributed by Mario Carneiro, 22-Jan-2015.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ) & ⊢ 𝐼 = (𝑥 ∈ (1...𝑁) ↦ sup((# “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < )) & ⊢ 𝐽 = (𝑥 ∈ (1...𝑁) ↦ sup((# “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , ◡ < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < )) & ⊢ 𝑇 = (𝑛 ∈ (1...𝑁) ↦ 〈(𝐼‘𝑛), (𝐽‘𝑛)〉) ⇒ ⊢ (𝜑 → 𝑇:(1...𝑁)–1-1→(ℕ × ℕ)) | ||
Theorem | erdszelem10 31308* | Lemma for erdsze 31310. (Contributed by Mario Carneiro, 22-Jan-2015.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ) & ⊢ 𝐼 = (𝑥 ∈ (1...𝑁) ↦ sup((# “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < )) & ⊢ 𝐽 = (𝑥 ∈ (1...𝑁) ↦ sup((# “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , ◡ < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < )) & ⊢ 𝑇 = (𝑛 ∈ (1...𝑁) ↦ 〈(𝐼‘𝑛), (𝐽‘𝑛)〉) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑆 ∈ ℕ) & ⊢ (𝜑 → ((𝑅 − 1) · (𝑆 − 1)) < 𝑁) ⇒ ⊢ (𝜑 → ∃𝑚 ∈ (1...𝑁)(¬ (𝐼‘𝑚) ∈ (1...(𝑅 − 1)) ∨ ¬ (𝐽‘𝑚) ∈ (1...(𝑆 − 1)))) | ||
Theorem | erdszelem11 31309* | Lemma for erdsze 31310. (Contributed by Mario Carneiro, 22-Jan-2015.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ) & ⊢ 𝐼 = (𝑥 ∈ (1...𝑁) ↦ sup((# “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < )) & ⊢ 𝐽 = (𝑥 ∈ (1...𝑁) ↦ sup((# “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , ◡ < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < )) & ⊢ 𝑇 = (𝑛 ∈ (1...𝑁) ↦ 〈(𝐼‘𝑛), (𝐽‘𝑛)〉) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑆 ∈ ℕ) & ⊢ (𝜑 → ((𝑅 − 1) · (𝑆 − 1)) < 𝑁) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 (1...𝑁)((𝑅 ≤ (#‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , < (𝑠, (𝐹 “ 𝑠))) ∨ (𝑆 ≤ (#‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , ◡ < (𝑠, (𝐹 “ 𝑠))))) | ||
Theorem | erdsze 31310* | The Erdős-Szekeres theorem. For any injective sequence 𝐹 on the reals of length at least (𝑅 − 1) · (𝑆 − 1) + 1, there is either a subsequence of length at least 𝑅 on which 𝐹 is increasing (i.e. a < , < order isomorphism) or a subsequence of length at least 𝑆 on which 𝐹 is decreasing (i.e. a < , ◡ < order isomorphism, recalling that ◡ < is the greater-than relation). This is part of Metamath 100 proof #73. (Contributed by Mario Carneiro, 22-Jan-2015.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑆 ∈ ℕ) & ⊢ (𝜑 → ((𝑅 − 1) · (𝑆 − 1)) < 𝑁) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 (1...𝑁)((𝑅 ≤ (#‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , < (𝑠, (𝐹 “ 𝑠))) ∨ (𝑆 ≤ (#‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , ◡ < (𝑠, (𝐹 “ 𝑠))))) | ||
Theorem | erdsze2lem1 31311* | Lemma for erdsze2 31313. (Contributed by Mario Carneiro, 22-Jan-2015.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑆 ∈ ℕ) & ⊢ (𝜑 → 𝐹:𝐴–1-1→ℝ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝑁 = ((𝑅 − 1) · (𝑆 − 1)) & ⊢ (𝜑 → 𝑁 < (#‘𝐴)) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:(1...(𝑁 + 1))–1-1→𝐴 ∧ 𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓))) | ||
Theorem | erdsze2lem2 31312* | Lemma for erdsze2 31313. (Contributed by Mario Carneiro, 22-Jan-2015.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑆 ∈ ℕ) & ⊢ (𝜑 → 𝐹:𝐴–1-1→ℝ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝑁 = ((𝑅 − 1) · (𝑆 − 1)) & ⊢ (𝜑 → 𝑁 < (#‘𝐴)) & ⊢ (𝜑 → 𝐺:(1...(𝑁 + 1))–1-1→𝐴) & ⊢ (𝜑 → 𝐺 Isom < , < ((1...(𝑁 + 1)), ran 𝐺)) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 𝐴((𝑅 ≤ (#‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , < (𝑠, (𝐹 “ 𝑠))) ∨ (𝑆 ≤ (#‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , ◡ < (𝑠, (𝐹 “ 𝑠))))) | ||
Theorem | erdsze2 31313* | Generalize the statement of the Erdős-Szekeres theorem erdsze 31310 to "sequences" indexed by an arbitrary subset of ℝ, which can be infinite. This is part of Metamath 100 proof #73. (Contributed by Mario Carneiro, 22-Jan-2015.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑆 ∈ ℕ) & ⊢ (𝜑 → 𝐹:𝐴–1-1→ℝ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → ((𝑅 − 1) · (𝑆 − 1)) < (#‘𝐴)) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 𝐴((𝑅 ≤ (#‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , < (𝑠, (𝐹 “ 𝑠))) ∨ (𝑆 ≤ (#‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , ◡ < (𝑠, (𝐹 “ 𝑠))))) | ||
Theorem | kur14lem1 31314 | Lemma for kur14 31324. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ 𝐴 ⊆ 𝑋 & ⊢ (𝑋 ∖ 𝐴) ∈ 𝑇 & ⊢ (𝐾‘𝐴) ∈ 𝑇 ⇒ ⊢ (𝑁 = 𝐴 → (𝑁 ⊆ 𝑋 ∧ {(𝑋 ∖ 𝑁), (𝐾‘𝑁)} ⊆ 𝑇)) | ||
Theorem | kur14lem2 31315 | Lemma for kur14 31324. Write interior in terms of closure and complement: 𝑖𝐴 = 𝑐𝑘𝑐𝐴 where 𝑐 is complement and 𝑘 is closure. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) & ⊢ 𝐼 = (int‘𝐽) & ⊢ 𝐴 ⊆ 𝑋 ⇒ ⊢ (𝐼‘𝐴) = (𝑋 ∖ (𝐾‘(𝑋 ∖ 𝐴))) | ||
Theorem | kur14lem3 31316 | Lemma for kur14 31324. A closure is a subset of the base set. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) & ⊢ 𝐼 = (int‘𝐽) & ⊢ 𝐴 ⊆ 𝑋 ⇒ ⊢ (𝐾‘𝐴) ⊆ 𝑋 | ||
Theorem | kur14lem4 31317 | Lemma for kur14 31324. Complementation is an involution on the set of subsets of a topology. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) & ⊢ 𝐼 = (int‘𝐽) & ⊢ 𝐴 ⊆ 𝑋 ⇒ ⊢ (𝑋 ∖ (𝑋 ∖ 𝐴)) = 𝐴 | ||
Theorem | kur14lem5 31318 | Lemma for kur14 31324. Closure is an idempotent operation in the set of subsets of a topology. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) & ⊢ 𝐼 = (int‘𝐽) & ⊢ 𝐴 ⊆ 𝑋 ⇒ ⊢ (𝐾‘(𝐾‘𝐴)) = (𝐾‘𝐴) | ||
Theorem | kur14lem6 31319 | Lemma for kur14 31324. If 𝑘 is the complementation operator and 𝑘 is the closure operator, this expresses the identity 𝑘𝑐𝑘𝐴 = 𝑘𝑐𝑘𝑐𝑘𝑐𝑘𝐴 for any subset 𝐴 of the topological space. This is the key result that lets us cut down long enough sequences of 𝑐𝑘𝑐𝑘... that arise when applying closure and complement repeatedly to 𝐴, and explains why we end up with a number as large as 14, yet no larger. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) & ⊢ 𝐼 = (int‘𝐽) & ⊢ 𝐴 ⊆ 𝑋 & ⊢ 𝐵 = (𝑋 ∖ (𝐾‘𝐴)) ⇒ ⊢ (𝐾‘(𝐼‘(𝐾‘𝐵))) = (𝐾‘𝐵) | ||
Theorem | kur14lem7 31320 | Lemma for kur14 31324: main proof. The set 𝑇 here contains all the distinct combinations of 𝑘 and 𝑐 that can arise, and we prove here that applying 𝑘 or 𝑐 to any element of 𝑇 yields another elemnt of 𝑇. In operator shorthand, we have 𝑇 = {𝐴, 𝑐𝐴, 𝑘𝐴 , 𝑐𝑘𝐴, 𝑘𝑐𝐴, 𝑐𝑘𝑐𝐴, 𝑘𝑐𝑘𝐴, 𝑐𝑘𝑐𝑘𝐴, 𝑘𝑐𝑘𝑐𝐴, 𝑐𝑘𝑐𝑘𝑐𝐴, 𝑘𝑐𝑘𝑐𝑘𝐴, 𝑐𝑘𝑐𝑘𝑐𝑘𝐴, 𝑘𝑐𝑘𝑐𝑘𝑐𝐴, 𝑐𝑘𝑐𝑘𝑐𝑘𝑐𝐴}. From the identities 𝑐𝑐𝐴 = 𝐴 and 𝑘𝑘𝐴 = 𝑘𝐴, we can reduce any operator combination containing two adjacent identical operators, which is why the list only contains alternating sequences. The reason the sequences don't keep going after a certain point is due to the identity 𝑘𝑐𝑘𝐴 = 𝑘𝑐𝑘𝑐𝑘𝑐𝑘𝐴, proved in kur14lem6 31319. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) & ⊢ 𝐼 = (int‘𝐽) & ⊢ 𝐴 ⊆ 𝑋 & ⊢ 𝐵 = (𝑋 ∖ (𝐾‘𝐴)) & ⊢ 𝐶 = (𝐾‘(𝑋 ∖ 𝐴)) & ⊢ 𝐷 = (𝐼‘(𝐾‘𝐴)) & ⊢ 𝑇 = ((({𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} ∪ {𝐵, 𝐶, (𝐼‘𝐴)}) ∪ {(𝐾‘𝐵), 𝐷, (𝐾‘(𝐼‘𝐴))}) ∪ ({(𝐼‘𝐶), (𝐾‘𝐷), (𝐼‘(𝐾‘𝐵))} ∪ {(𝐾‘(𝐼‘𝐶)), (𝐼‘(𝐾‘(𝐼‘𝐴)))})) ⇒ ⊢ (𝑁 ∈ 𝑇 → (𝑁 ⊆ 𝑋 ∧ {(𝑋 ∖ 𝑁), (𝐾‘𝑁)} ⊆ 𝑇)) | ||
Theorem | kur14lem8 31321 | Lemma for kur14 31324. Show that the set 𝑇 contains at most 14 elements. (It could be less if some of the operators take the same value for a given set, but Kuratowski showed that this upper bound of 14 is tight in the sense that there exist topological spaces and subsets of these spaces for which all 14 generated sets are distinct, and indeed the real numbers form such a topological space.) (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) & ⊢ 𝐼 = (int‘𝐽) & ⊢ 𝐴 ⊆ 𝑋 & ⊢ 𝐵 = (𝑋 ∖ (𝐾‘𝐴)) & ⊢ 𝐶 = (𝐾‘(𝑋 ∖ 𝐴)) & ⊢ 𝐷 = (𝐼‘(𝐾‘𝐴)) & ⊢ 𝑇 = ((({𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} ∪ {𝐵, 𝐶, (𝐼‘𝐴)}) ∪ {(𝐾‘𝐵), 𝐷, (𝐾‘(𝐼‘𝐴))}) ∪ ({(𝐼‘𝐶), (𝐾‘𝐷), (𝐼‘(𝐾‘𝐵))} ∪ {(𝐾‘(𝐼‘𝐶)), (𝐼‘(𝐾‘(𝐼‘𝐴)))})) ⇒ ⊢ (𝑇 ∈ Fin ∧ (#‘𝑇) ≤ ;14) | ||
Theorem | kur14lem9 31322* | Lemma for kur14 31324. Since the set 𝑇 is closed under closure and complement, it contains the minimal set 𝑆 as a subset, so 𝑆 also has at most 14 elements. (Indeed 𝑆 = 𝑇, and it's not hard to prove this, but we don't need it for this proof.) (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) & ⊢ 𝐼 = (int‘𝐽) & ⊢ 𝐴 ⊆ 𝑋 & ⊢ 𝐵 = (𝑋 ∖ (𝐾‘𝐴)) & ⊢ 𝐶 = (𝐾‘(𝑋 ∖ 𝐴)) & ⊢ 𝐷 = (𝐼‘(𝐾‘𝐴)) & ⊢ 𝑇 = ((({𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} ∪ {𝐵, 𝐶, (𝐼‘𝐴)}) ∪ {(𝐾‘𝐵), 𝐷, (𝐾‘(𝐼‘𝐴))}) ∪ ({(𝐼‘𝐶), (𝐾‘𝐷), (𝐼‘(𝐾‘𝐵))} ∪ {(𝐾‘(𝐼‘𝐶)), (𝐼‘(𝐾‘(𝐼‘𝐴)))})) & ⊢ 𝑆 = ∩ {𝑥 ∈ 𝒫 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥)} ⇒ ⊢ (𝑆 ∈ Fin ∧ (#‘𝑆) ≤ ;14) | ||
Theorem | kur14lem10 31323* | Lemma for kur14 31324. Discharge the set 𝑇. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) & ⊢ 𝑆 = ∩ {𝑥 ∈ 𝒫 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥)} & ⊢ 𝐴 ⊆ 𝑋 ⇒ ⊢ (𝑆 ∈ Fin ∧ (#‘𝑆) ≤ ;14) | ||
Theorem | kur14 31324* | Kuratowski's closure-complement theorem. There are at most 14 sets which can be obtained by the application of the closure and complement operations to a set in a topological space. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) & ⊢ 𝑆 = ∩ {𝑥 ∈ 𝒫 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥)} ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (𝑆 ∈ Fin ∧ (#‘𝑆) ≤ ;14)) | ||
Syntax | cretr 31325 | Extend class notation with the retract relation. |
class Retr | ||
Definition | df-retr 31326* | Define the set of retractions on two topological spaces. We say that 𝑅 is a retraction from 𝐽 to 𝐾. or 𝑅 ∈ (𝐽 Retr 𝐾) iff there is an 𝑆 such that 𝑅:𝐽⟶𝐾, 𝑆:𝐾⟶𝐽 are continuous functions called the retraction and section respectively, and their composite 𝑅 ∘ 𝑆 is homotopic to the identity map. If a retraction exists, we say 𝐽 is a retract of 𝐾. (This terminology is borrowed from HoTT and appears to be nonstandard, although it has similaries to the concept of retract in the category of topological spaces and to a deformation retract in general topology.) Two topological spaces that are retracts of each other are called homotopy equivalent. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ Retr = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑟 ∈ (𝑗 Cn 𝑘) ∣ ∃𝑠 ∈ (𝑘 Cn 𝑗)((𝑟 ∘ 𝑠)(𝑗 Htpy 𝑗)( I ↾ ∪ 𝑗)) ≠ ∅}) | ||
Syntax | cpconn 31327 | Extend class notation with the class of path-connected topologies. |
class PConn | ||
Syntax | csconn 31328 | Extend class notation with the class of simply connected topologies. |
class SConn | ||
Definition | df-pconn 31329* | Define the class of path-connected topologies. A topology is path-connected if there is a path (a continuous function from the unit interval) that goes from 𝑥 to 𝑦 for any points 𝑥, 𝑦 in the space. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ PConn = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} | ||
Definition | df-sconn 31330* | Define the class of simply connected topologies. A topology is simply connected if it is path-connected and every loop (continuous path with identical start and endpoint) is contractible to a point (path-homotopic to a constant function). (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ SConn = {𝑗 ∈ PConn ∣ ∀𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)}))} | ||
Theorem | ispconn 31331* | The property of being a path-connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ PConn ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦))) | ||
Theorem | pconncn 31332* | The property of being a path-connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝐴 ∧ (𝑓‘1) = 𝐵)) | ||
Theorem | pconntop 31333 | A simply connected space is a topology. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝐽 ∈ PConn → 𝐽 ∈ Top) | ||
Theorem | issconn 31334* | The property of being a simply connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝐽 ∈ SConn ↔ (𝐽 ∈ PConn ∧ ∀𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝐽)((0[,]1) × {(𝑓‘0)})))) | ||
Theorem | sconnpconn 31335 | A simply connected space is path-connected. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝐽 ∈ SConn → 𝐽 ∈ PConn) | ||
Theorem | sconntop 31336 | A simply connected space is a topology. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝐽 ∈ SConn → 𝐽 ∈ Top) | ||
Theorem | sconnpht 31337 | A closed path in a simply connected space is contractible to a point. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ ((𝐽 ∈ SConn ∧ 𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = (𝐹‘1)) → 𝐹( ≃ph‘𝐽)((0[,]1) × {(𝐹‘0)})) | ||
Theorem | cnpconn 31338 | An image of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ ((𝐽 ∈ PConn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ PConn) | ||
Theorem | pconnconn 31339 | A path-connected space is connected. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝐽 ∈ PConn → 𝐽 ∈ Conn) | ||
Theorem | txpconn 31340 | The topological product of two path-connected spaces is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ ((𝑅 ∈ PConn ∧ 𝑆 ∈ PConn) → (𝑅 ×t 𝑆) ∈ PConn) | ||
Theorem | ptpconn 31341 | The topological product of a collection of path-connected spaces is path-connected. The proof uses the axiom of choice. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) → (∏t‘𝐹) ∈ PConn) | ||
Theorem | indispconn 31342 | The indiscrete topology (or trivial topology) on any set is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ {∅, 𝐴} ∈ PConn | ||
Theorem | connpconn 31343 | A connected and locally path-connected space is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015.) |
⊢ ((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn) → 𝐽 ∈ PConn) | ||
Theorem | qtoppconn 31344 | A quotient of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ PConn ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ PConn) | ||
Theorem | pconnpi1 31345 | All fundamental groups in a path-connected space are isomorphic. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑃 = (𝐽 π1 𝐴) & ⊢ 𝑄 = (𝐽 π1 𝐵) & ⊢ 𝑆 = (Base‘𝑃) & ⊢ 𝑇 = (Base‘𝑄) ⇒ ⊢ ((𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝑃 ≃𝑔 𝑄) | ||
Theorem | sconnpht2 31346 | Any two paths in a simply connected space with the same start and end point are path-homotopic. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ (𝜑 → 𝐽 ∈ SConn) & ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → (𝐹‘0) = (𝐺‘0)) & ⊢ (𝜑 → (𝐹‘1) = (𝐺‘1)) ⇒ ⊢ (𝜑 → 𝐹( ≃ph‘𝐽)𝐺) | ||
Theorem | sconnpi1 31347 | A path-connected topological space is simply connected iff its fundamental group is trivial. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋) → (𝐽 ∈ SConn ↔ (Base‘(𝐽 π1 𝑌)) ≈ 1𝑜)) | ||
Theorem | txsconnlem 31348 | Lemma for txsconn 31349. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ (𝜑 → 𝑅 ∈ Top) & ⊢ (𝜑 → 𝑆 ∈ Top) & ⊢ (𝜑 → 𝐹 ∈ (II Cn (𝑅 ×t 𝑆))) & ⊢ 𝐴 = ((1st ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝐹) & ⊢ 𝐵 = ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ (𝐴(PHtpy‘𝑅)((0[,]1) × {(𝐴‘0)}))) & ⊢ (𝜑 → 𝐻 ∈ (𝐵(PHtpy‘𝑆)((0[,]1) × {(𝐵‘0)}))) ⇒ ⊢ (𝜑 → 𝐹( ≃ph‘(𝑅 ×t 𝑆))((0[,]1) × {(𝐹‘0)})) | ||
Theorem | txsconn 31349 | The topological product of two simply connected spaces is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ ((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) → (𝑅 ×t 𝑆) ∈ SConn) | ||
Theorem | cvxpconn 31350* | A convex subset of the complex numbers is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆) & ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝑆) ⇒ ⊢ (𝜑 → 𝐾 ∈ PConn) | ||
Theorem | cvxsconn 31351* | A convex subset of the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆) & ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝑆) ⇒ ⊢ (𝜑 → 𝐾 ∈ SConn) | ||
Theorem | blsconn 31352 | An open ball in the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝑆 = (𝑃(ball‘(abs ∘ − ))𝑅) & ⊢ 𝐾 = (𝐽 ↾t 𝑆) ⇒ ⊢ ((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*) → 𝐾 ∈ SConn) | ||
Theorem | cnllysconn 31353 | The topology of the complex numbers is locally simply connected. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ Locally SConn | ||
Theorem | resconn 31354 | A subset of ℝ is simply connected iff it is connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 𝐽 = ((topGen‘ran (,)) ↾t 𝐴) ⇒ ⊢ (𝐴 ⊆ ℝ → (𝐽 ∈ SConn ↔ 𝐽 ∈ Conn)) | ||
Theorem | ioosconn 31355 | An open interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ ((topGen‘ran (,)) ↾t (𝐴(,)𝐵)) ∈ SConn | ||
Theorem | iccsconn 31356 | A closed interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ SConn) | ||
Theorem | retopsconn 31357 | The real numbers are simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ (topGen‘ran (,)) ∈ SConn | ||
Theorem | iccllysconn 31358 | A closed interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Locally SConn) | ||
Theorem | rellysconn 31359 | The real numbers are locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ (topGen‘ran (,)) ∈ Locally SConn | ||
Theorem | iisconn 31360 | The unit interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ II ∈ SConn | ||
Theorem | iillysconn 31361 | The unit interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ II ∈ Locally SConn | ||
Theorem | iinllyconn 31362 | The unit interval is locally connected. (Contributed by Mario Carneiro, 6-Jul-2015.) |
⊢ II ∈ 𝑛-Locally Conn | ||
Syntax | ccvm 31363 | Extend class notation with the class of covering maps. |
class CovMap | ||
Definition | df-cvm 31364* | Define the class of covering maps on two topological spaces. A function 𝑓:𝑐⟶𝑗 is a covering map if it is continuous and for every point 𝑥 in the target space there is a neighborhood 𝑘 of 𝑥 and a decomposition 𝑠 of the preimage of 𝑘 as a disjoint union such that 𝑓 is a homeomorphism of each set 𝑢 ∈ 𝑠 onto 𝑘. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ CovMap = (𝑐 ∈ Top, 𝑗 ∈ Top ↦ {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑘 ∈ 𝑗 (𝑥 ∈ 𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})(∪ 𝑠 = (◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘)))))}) | ||
Theorem | fncvm 31365 | Lemma for covering maps. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ CovMap Fn (Top × Top) | ||
Theorem | cvmscbv 31366* | Change bound variables in the set of even coverings. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ 𝑆 = (𝑎 ∈ 𝐽 ↦ {𝑏 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑏 = (◡𝐹 “ 𝑎) ∧ ∀𝑐 ∈ 𝑏 (∀𝑑 ∈ (𝑏 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑎))))}) | ||
Theorem | iscvm 31367* | The property of being a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) ↔ ((𝐶 ∈ Top ∧ 𝐽 ∈ Top ∧ 𝐹 ∈ (𝐶 Cn 𝐽)) ∧ ∀𝑥 ∈ 𝑋 ∃𝑘 ∈ 𝐽 (𝑥 ∈ 𝑘 ∧ (𝑆‘𝑘) ≠ ∅))) | ||
Theorem | cvmtop1 31368 | Reverse closure for a covering map. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) | ||
Theorem | cvmtop2 31369 | Reverse closure for a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top) | ||
Theorem | cvmcn 31370 | A covering map is a continuous function. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽)) | ||
Theorem | cvmcov 31371* | Property of a covering map. In order to make the covering property more manageable, we define here the set 𝑆(𝑘) of all even coverings of an open set 𝑘 in the range. Then the covering property states that every point has a neighborhood which has an even covering. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑃 ∈ 𝑋) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝑆‘𝑥) ≠ ∅)) | ||
Theorem | cvmsrcl 31372* | Reverse closure for an even covering. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑈 ∈ 𝐽) | ||
Theorem | cvmsi 31373* | One direction of cvmsval 31374. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ (𝑇 ∈ (𝑆‘𝑈) → (𝑈 ∈ 𝐽 ∧ (𝑇 ⊆ 𝐶 ∧ 𝑇 ≠ ∅) ∧ (∪ 𝑇 = (◡𝐹 “ 𝑈) ∧ ∀𝑢 ∈ 𝑇 (∀𝑣 ∈ (𝑇 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑈)))))) | ||
Theorem | cvmsval 31374* | Elementhood in the set 𝑆 of all even coverings of an open set in 𝐽. 𝑆 is an even covering of 𝑈 if it is a nonempty collection of disjoint open sets in 𝐶 whose union is the preimage of 𝑈, such that each set 𝑢 ∈ 𝑆 is homeomorphic under 𝐹 to 𝑈. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ (𝐶 ∈ 𝑉 → (𝑇 ∈ (𝑆‘𝑈) ↔ (𝑈 ∈ 𝐽 ∧ (𝑇 ⊆ 𝐶 ∧ 𝑇 ≠ ∅) ∧ (∪ 𝑇 = (◡𝐹 “ 𝑈) ∧ ∀𝑢 ∈ 𝑇 (∀𝑣 ∈ (𝑇 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑈))))))) | ||
Theorem | cvmsss 31375* | An even covering is a subset of the topology of the domain (i.e. a collection of open sets). (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑇 ⊆ 𝐶) | ||
Theorem | cvmsn0 31376* | An even covering is nonempty. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑇 ≠ ∅) | ||
Theorem | cvmsuni 31377* | An even covering of 𝑈 has union equal to the preimage of 𝑈 by 𝐹. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ (𝑇 ∈ (𝑆‘𝑈) → ∪ 𝑇 = (◡𝐹 “ 𝑈)) | ||
Theorem | cvmsdisj 31378* | An even covering of 𝑈 is a disjoint union. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ ((𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇) → (𝐴 = 𝐵 ∨ (𝐴 ∩ 𝐵) = ∅)) | ||
Theorem | cvmshmeo 31379* | Every element of an even covering of 𝑈 is homeomorphic to 𝑈 via 𝐹. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ ((𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝑇) → (𝐹 ↾ 𝐴) ∈ ((𝐶 ↾t 𝐴)Homeo(𝐽 ↾t 𝑈))) | ||
Theorem | cvmsf1o 31380* | 𝐹, localized to an element of an even covering of 𝑈, is a bijection. (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝑇) → (𝐹 ↾ 𝐴):𝐴–1-1-onto→𝑈) | ||
Theorem | cvmscld 31381* | The sets of an even covering are clopen in the subspace topology on 𝑇. (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝑇) → 𝐴 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈)))) | ||
Theorem | cvmsss2 31382* | An open subset of an evenly covered set is evenly covered. (Contributed by Mario Carneiro, 7-Jul-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) → ((𝑆‘𝑈) ≠ ∅ → (𝑆‘𝑉) ≠ ∅)) | ||
Theorem | cvmcov2 31383* | The covering map property can be restricted to an open subset. (Contributed by Mario Carneiro, 7-Jul-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑥 ∈ 𝒫 𝑈(𝑃 ∈ 𝑥 ∧ (𝑆‘𝑥) ≠ ∅)) | ||
Theorem | cvmseu 31384* | Every element in ∪ 𝑇 is a member of a unique element of 𝑇. (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 ⇒ ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → ∃!𝑥 ∈ 𝑇 𝐴 ∈ 𝑥) | ||
Theorem | cvmsiota 31385* | Identify the unique element of 𝑇 containing 𝐴. (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑊 = (℩𝑥 ∈ 𝑇 𝐴 ∈ 𝑥) ⇒ ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → (𝑊 ∈ 𝑇 ∧ 𝐴 ∈ 𝑊)) | ||
Theorem | cvmopnlem 31386* | Lemma for cvmopn 31388. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 ⇒ ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (𝐹 “ 𝐴) ∈ 𝐽) | ||
Theorem | cvmfolem 31387* | Lemma for cvmfo 31408. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹:𝐵–onto→𝑋) | ||
Theorem | cvmopn 31388 | A covering map is an open map. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (𝐹 “ 𝐴) ∈ 𝐽) | ||
Theorem | cvmliftmolem1 31389* | Lemma for cvmliftmo 31392. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ Conn) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Conn) & ⊢ (𝜑 → 𝑂 ∈ 𝑌) & ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶)) & ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶)) & ⊢ (𝜑 → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁)) & ⊢ (𝜑 → (𝑀‘𝑂) = (𝑁‘𝑂)) & ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ∈ (𝑆‘𝑈)) & ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝑇) & ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ 𝑊)) & ⊢ ((𝜑 ∧ 𝜓) → (𝐾 ↾t 𝐼) ∈ Conn) & ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐼) & ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝐼) & ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝐼) & ⊢ ((𝜑 ∧ 𝜓) → (𝐹‘(𝑀‘𝑋)) ∈ 𝑈) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) → 𝑅 ∈ dom (𝑀 ∩ 𝑁))) | ||
Theorem | cvmliftmolem2 31390* | Lemma for cvmliftmo 31392. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ Conn) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Conn) & ⊢ (𝜑 → 𝑂 ∈ 𝑌) & ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶)) & ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶)) & ⊢ (𝜑 → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁)) & ⊢ (𝜑 → (𝑀‘𝑂) = (𝑁‘𝑂)) & ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ (𝜑 → 𝑀 = 𝑁) | ||
Theorem | cvmliftmoi 31391 | A lift of a continuous function from a connected and locally connected space over a covering map is unique when it exists. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ Conn) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Conn) & ⊢ (𝜑 → 𝑂 ∈ 𝑌) & ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶)) & ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶)) & ⊢ (𝜑 → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁)) & ⊢ (𝜑 → (𝑀‘𝑂) = (𝑁‘𝑂)) ⇒ ⊢ (𝜑 → 𝑀 = 𝑁) | ||
Theorem | cvmliftmo 31392* | A lift of a continuous function from a connected and locally connected space over a covering map is unique when it exists. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by NM, 17-Jun-2017.) |
⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ Conn) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Conn) & ⊢ (𝜑 → 𝑂 ∈ 𝑌) & ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂)) ⇒ ⊢ (𝜑 → ∃*𝑓 ∈ (𝐾 Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘𝑂) = 𝑃)) | ||
Theorem | cvmliftlem1 31393* | Lemma for cvmlift 31407. In cvmliftlem15 31406, we picked an 𝑁 large enough so that the sections (𝐺 “ [(𝑘 − 1) / 𝑁, 𝑘 / 𝑁]) are all contained in an even covering, and the function 𝑇 enumerates these even coverings. So 1st ‘(𝑇‘𝑀) is a neighborhood of (𝐺 “ [(𝑀 − 1) / 𝑁, 𝑀 / 𝑁]), and 2nd ‘(𝑇‘𝑀) is an even covering of 1st ‘(𝑇‘𝑀), which is to say a disjoint union of open sets in 𝐶 whose image is 1st ‘(𝑇‘𝑀). (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))) & ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘))) & ⊢ 𝐿 = (topGen‘ran (,)) & ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ (1...𝑁)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (2nd ‘(𝑇‘𝑀)) ∈ (𝑆‘(1st ‘(𝑇‘𝑀)))) | ||
Theorem | cvmliftlem2 31394* | Lemma for cvmlift 31407. 𝑊 = [(𝑘 − 1) / 𝑁, 𝑘 / 𝑁] is a subset of [0, 1] for each 𝑀 ∈ (1...𝑁). (Contributed by Mario Carneiro, 16-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))) & ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘))) & ⊢ 𝐿 = (topGen‘ran (,)) & ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ (1...𝑁)) & ⊢ 𝑊 = (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ⊆ (0[,]1)) | ||
Theorem | cvmliftlem3 31395* | Lemma for cvmlift 31407. Since 1st ‘(𝑇‘𝑀) is a neighborhood of (𝐺 “ 𝑊), every element 𝐴 ∈ 𝑊 satisfies (𝐺‘𝐴) ∈ (1st ‘(𝑇‘𝑀)). (Contributed by Mario Carneiro, 16-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))) & ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘))) & ⊢ 𝐿 = (topGen‘ran (,)) & ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ (1...𝑁)) & ⊢ 𝑊 = (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝑊) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝐺‘𝐴) ∈ (1st ‘(𝑇‘𝑀))) | ||
Theorem | cvmliftlem4 31396* | Lemma for cvmlift 31407. The function 𝑄 will be our lifted path, defined piecewise on each section [(𝑀 − 1) / 𝑁, 𝑀 / 𝑁] for 𝑀 ∈ (1...𝑁). For 𝑀 = 0, it is a "seed" value which makes the rest of the recursion work, a singleton function mapping 0 to 𝑃. (Contributed by Mario Carneiro, 15-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))) & ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘))) & ⊢ 𝐿 = (topGen‘ran (,)) & ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {〈0, {〈0, 𝑃〉}〉})) ⇒ ⊢ (𝑄‘0) = {〈0, 𝑃〉} | ||
Theorem | cvmliftlem5 31397* | Lemma for cvmlift 31407. Definition of 𝑄 at a successor. This is a function defined on 𝑊 as ◡(𝑇 ↾ 𝐼) ∘ 𝐺 where 𝐼 is the unique covering set of 2nd ‘(𝑇‘𝑀) that contains 𝑄(𝑀 − 1) evaluated at the last defined point, namely (𝑀 − 1) / 𝑁 (note that for 𝑀 = 1 this is using the seed value 𝑄(0)(0) = 𝑃). (Contributed by Mario Carneiro, 15-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))) & ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘))) & ⊢ 𝐿 = (topGen‘ran (,)) & ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {〈0, {〈0, 𝑃〉}〉})) & ⊢ 𝑊 = (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁)) ⇒ ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝑄‘𝑀) = (𝑧 ∈ 𝑊 ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))) | ||
Theorem | cvmliftlem6 31398* | Lemma for cvmlift 31407. Induction step for cvmliftlem7 31399. Assuming that 𝑄(𝑀 − 1) is defined at (𝑀 − 1) / 𝑁 and is a preimage of 𝐺((𝑀 − 1) / 𝑁), the next segment 𝑄(𝑀) is also defined and is a function on 𝑊 which is a lift 𝐺 for this segment. This follows explicitly from the definition 𝑄(𝑀) = ◡(𝐹 ↾ 𝐼) ∘ 𝐺 since 𝐺 is in 1st ‘(𝐹‘𝑀) for the entire interval so that ◡(𝐹 ↾ 𝐼) maps this into 𝐼 and 𝐹 ∘ 𝑄 maps back to 𝐺. (Contributed by Mario Carneiro, 16-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))) & ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘))) & ⊢ 𝐿 = (topGen‘ran (,)) & ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {〈0, {〈0, 𝑃〉}〉})) & ⊢ 𝑊 = (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ (1...𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))})) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ((𝑄‘𝑀):𝑊⟶𝐵 ∧ (𝐹 ∘ (𝑄‘𝑀)) = (𝐺 ↾ 𝑊))) | ||
Theorem | cvmliftlem7 31399* | Lemma for cvmlift 31407. Prove by induction that every 𝑄 function is well-defined (we can immediately follow this theorem with cvmliftlem6 31398 to show functionality and lifting of 𝑄). (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))) & ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘))) & ⊢ 𝐿 = (topGen‘ran (,)) & ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {〈0, {〈0, 𝑃〉}〉})) & ⊢ 𝑊 = (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁)) ⇒ ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))})) | ||
Theorem | cvmliftlem8 31400* | Lemma for cvmlift 31407. The functions 𝑄 are continuous functions because they are defined as ◡(𝐹 ↾ 𝐼) ∘ 𝐺 where 𝐺 is continuous and (𝐹 ↾ 𝐼) is a homeomorphism. (Contributed by Mario Carneiro, 16-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))) & ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘))) & ⊢ 𝐿 = (topGen‘ran (,)) & ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {〈0, {〈0, 𝑃〉}〉})) & ⊢ 𝑊 = (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁)) ⇒ ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑄‘𝑀) ∈ ((𝐿 ↾t 𝑊) Cn 𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |