| Metamath
Proof Explorer Theorem List (p. 353 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | erdszelem6 35201* | Lemma for erdsze 35207. (Contributed by Mario Carneiro, 22-Jan-2015.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ) & ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < )) & ⊢ 𝑂 Or ℝ ⇒ ⊢ (𝜑 → 𝐾:(1...𝑁)⟶ℕ) | ||
| Theorem | erdszelem7 35202* | Lemma for erdsze 35207. (Contributed by Mario Carneiro, 22-Jan-2015.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ) & ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < )) & ⊢ 𝑂 Or ℝ & ⊢ (𝜑 → 𝐴 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → ¬ (𝐾‘𝐴) ∈ (1...(𝑅 − 1))) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 (1...𝑁)(𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠)))) | ||
| Theorem | erdszelem8 35203* | Lemma for erdsze 35207. (Contributed by Mario Carneiro, 22-Jan-2015.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ) & ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < )) & ⊢ 𝑂 Or ℝ & ⊢ (𝜑 → 𝐴 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → ((𝐾‘𝐴) = (𝐾‘𝐵) → ¬ (𝐹‘𝐴)𝑂(𝐹‘𝐵))) | ||
| Theorem | erdszelem9 35204* | Lemma for erdsze 35207. (Contributed by Mario Carneiro, 22-Jan-2015.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ) & ⊢ 𝐼 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < )) & ⊢ 𝐽 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , ◡ < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < )) & ⊢ 𝑇 = (𝑛 ∈ (1...𝑁) ↦ 〈(𝐼‘𝑛), (𝐽‘𝑛)〉) ⇒ ⊢ (𝜑 → 𝑇:(1...𝑁)–1-1→(ℕ × ℕ)) | ||
| Theorem | erdszelem10 35205* | Lemma for erdsze 35207. (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 35206* | Lemma for erdsze 35207. (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 35207* | 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 35208* | Lemma for erdsze2 35210. (Contributed by Mario Carneiro, 22-Jan-2015.) |
| ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑆 ∈ ℕ) & ⊢ (𝜑 → 𝐹:𝐴–1-1→ℝ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝑁 = ((𝑅 − 1) · (𝑆 − 1)) & ⊢ (𝜑 → 𝑁 < (♯‘𝐴)) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:(1...(𝑁 + 1))–1-1→𝐴 ∧ 𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓))) | ||
| Theorem | erdsze2lem2 35209* | Lemma for erdsze2 35210. (Contributed by Mario Carneiro, 22-Jan-2015.) |
| ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑆 ∈ ℕ) & ⊢ (𝜑 → 𝐹:𝐴–1-1→ℝ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝑁 = ((𝑅 − 1) · (𝑆 − 1)) & ⊢ (𝜑 → 𝑁 < (♯‘𝐴)) & ⊢ (𝜑 → 𝐺:(1...(𝑁 + 1))–1-1→𝐴) & ⊢ (𝜑 → 𝐺 Isom < , < ((1...(𝑁 + 1)), ran 𝐺)) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 𝐴((𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , < (𝑠, (𝐹 “ 𝑠))) ∨ (𝑆 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , ◡ < (𝑠, (𝐹 “ 𝑠))))) | ||
| Theorem | erdsze2 35210* | Generalize the statement of the Erdős-Szekeres theorem erdsze 35207 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 35211 | Lemma for kur14 35221. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ 𝐴 ⊆ 𝑋 & ⊢ (𝑋 ∖ 𝐴) ∈ 𝑇 & ⊢ (𝐾‘𝐴) ∈ 𝑇 ⇒ ⊢ (𝑁 = 𝐴 → (𝑁 ⊆ 𝑋 ∧ {(𝑋 ∖ 𝑁), (𝐾‘𝑁)} ⊆ 𝑇)) | ||
| Theorem | kur14lem2 35212 | Lemma for kur14 35221. 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 35213 | Lemma for kur14 35221. A closure is a subset of the base set. (Contributed by Mario Carneiro, 11-Feb-2015.) |
| ⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) & ⊢ 𝐼 = (int‘𝐽) & ⊢ 𝐴 ⊆ 𝑋 ⇒ ⊢ (𝐾‘𝐴) ⊆ 𝑋 | ||
| Theorem | kur14lem4 35214 | Lemma for kur14 35221. Complementation is an involution on the set of subsets of a topology. (Contributed by Mario Carneiro, 11-Feb-2015.) |
| ⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) & ⊢ 𝐼 = (int‘𝐽) & ⊢ 𝐴 ⊆ 𝑋 ⇒ ⊢ (𝑋 ∖ (𝑋 ∖ 𝐴)) = 𝐴 | ||
| Theorem | kur14lem5 35215 | Lemma for kur14 35221. 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 35216 | Lemma for kur14 35221. 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 35217 | Lemma for kur14 35221: 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 element 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 35216. (Contributed by Mario Carneiro, 11-Feb-2015.) |
| ⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) & ⊢ 𝐼 = (int‘𝐽) & ⊢ 𝐴 ⊆ 𝑋 & ⊢ 𝐵 = (𝑋 ∖ (𝐾‘𝐴)) & ⊢ 𝐶 = (𝐾‘(𝑋 ∖ 𝐴)) & ⊢ 𝐷 = (𝐼‘(𝐾‘𝐴)) & ⊢ 𝑇 = ((({𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} ∪ {𝐵, 𝐶, (𝐼‘𝐴)}) ∪ {(𝐾‘𝐵), 𝐷, (𝐾‘(𝐼‘𝐴))}) ∪ ({(𝐼‘𝐶), (𝐾‘𝐷), (𝐼‘(𝐾‘𝐵))} ∪ {(𝐾‘(𝐼‘𝐶)), (𝐼‘(𝐾‘(𝐼‘𝐴)))})) ⇒ ⊢ (𝑁 ∈ 𝑇 → (𝑁 ⊆ 𝑋 ∧ {(𝑋 ∖ 𝑁), (𝐾‘𝑁)} ⊆ 𝑇)) | ||
| Theorem | kur14lem8 35218 | Lemma for kur14 35221. 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 35219* | Lemma for kur14 35221. 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 35220* | Lemma for kur14 35221. Discharge the set 𝑇. (Contributed by Mario Carneiro, 11-Feb-2015.) |
| ⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (cls‘𝐽) & ⊢ 𝑆 = ∩ {𝑥 ∈ 𝒫 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥)} & ⊢ 𝐴 ⊆ 𝑋 ⇒ ⊢ (𝑆 ∈ Fin ∧ (♯‘𝑆) ≤ ;14) | ||
| Theorem | kur14 35221* | 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 35222 | Extend class notation with the retract relation. |
| class Retr | ||
| Definition | df-retr 35223* | 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 35224 | Extend class notation with the class of path-connected topologies. |
| class PConn | ||
| Syntax | csconn 35225 | Extend class notation with the class of simply connected topologies. |
| class SConn | ||
| Definition | df-pconn 35226* | Define the class of path-connected topologies. A topology is path-connected if there is a path (a continuous function from the closed 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 35227* | 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 35228* | The property of being a path-connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ PConn ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦))) | ||
| Theorem | pconncn 35229* | The property of being a path-connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝐴 ∧ (𝑓‘1) = 𝐵)) | ||
| Theorem | pconntop 35230 | A simply connected space is a topology. (Contributed by Mario Carneiro, 11-Feb-2015.) |
| ⊢ (𝐽 ∈ PConn → 𝐽 ∈ Top) | ||
| Theorem | issconn 35231* | 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 35232 | A simply connected space is path-connected. (Contributed by Mario Carneiro, 11-Feb-2015.) |
| ⊢ (𝐽 ∈ SConn → 𝐽 ∈ PConn) | ||
| Theorem | sconntop 35233 | A simply connected space is a topology. (Contributed by Mario Carneiro, 11-Feb-2015.) |
| ⊢ (𝐽 ∈ SConn → 𝐽 ∈ Top) | ||
| Theorem | sconnpht 35234 | 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 35235 | An image of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015.) |
| ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ ((𝐽 ∈ PConn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ PConn) | ||
| Theorem | pconnconn 35236 | A path-connected space is connected. (Contributed by Mario Carneiro, 11-Feb-2015.) |
| ⊢ (𝐽 ∈ PConn → 𝐽 ∈ Conn) | ||
| Theorem | txpconn 35237 | The topological product of two path-connected spaces is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015.) |
| ⊢ ((𝑅 ∈ PConn ∧ 𝑆 ∈ PConn) → (𝑅 ×t 𝑆) ∈ PConn) | ||
| Theorem | ptpconn 35238 | 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 35239 | 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 35240 | A connected and locally path-connected space is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015.) |
| ⊢ ((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn) → 𝐽 ∈ PConn) | ||
| Theorem | qtoppconn 35241 | A quotient of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ PConn ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ PConn) | ||
| Theorem | pconnpi1 35242 | All fundamental groups in a path-connected space are isomorphic. (Contributed by Mario Carneiro, 12-Feb-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑃 = (𝐽 π1 𝐴) & ⊢ 𝑄 = (𝐽 π1 𝐵) & ⊢ 𝑆 = (Base‘𝑃) & ⊢ 𝑇 = (Base‘𝑄) ⇒ ⊢ ((𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝑃 ≃𝑔 𝑄) | ||
| Theorem | sconnpht2 35243 | 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 35244 | 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 𝑌)) ≈ 1o)) | ||
| Theorem | txsconnlem 35245 | Lemma for txsconn 35246. (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 35246 | The topological product of two simply connected spaces is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.) |
| ⊢ ((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) → (𝑅 ×t 𝑆) ∈ SConn) | ||
| Theorem | cvxpconn 35247* | A convex subset of the complex numbers is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015.) Avoid ax-mulf 11235. (Revised by GG, 19-Apr-2025.) |
| ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆) & ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝑆) ⇒ ⊢ (𝜑 → 𝐾 ∈ PConn) | ||
| Theorem | cvxsconn 35248* | A convex subset of the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.) Avoid ax-mulf 11235. (Revised by GG, 19-Apr-2025.) |
| ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆) & ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝑆) ⇒ ⊢ (𝜑 → 𝐾 ∈ SConn) | ||
| Theorem | blsconn 35249 | 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 35250 | The topology of the complex numbers is locally simply connected. (Contributed by Mario Carneiro, 2-Mar-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ Locally SConn | ||
| Theorem | resconn 35251 | A subset of ℝ is simply connected iff it is connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
| ⊢ 𝐽 = ((topGen‘ran (,)) ↾t 𝐴) ⇒ ⊢ (𝐴 ⊆ ℝ → (𝐽 ∈ SConn ↔ 𝐽 ∈ Conn)) | ||
| Theorem | ioosconn 35252 | An open interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
| ⊢ ((topGen‘ran (,)) ↾t (𝐴(,)𝐵)) ∈ SConn | ||
| Theorem | iccsconn 35253 | A closed interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ SConn) | ||
| Theorem | retopsconn 35254 | The real numbers are simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
| ⊢ (topGen‘ran (,)) ∈ SConn | ||
| Theorem | iccllysconn 35255 | A closed interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Locally SConn) | ||
| Theorem | rellysconn 35256 | The real numbers are locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.) |
| ⊢ (topGen‘ran (,)) ∈ Locally SConn | ||
| Theorem | iisconn 35257 | The unit interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
| ⊢ II ∈ SConn | ||
| Theorem | iillysconn 35258 | The unit interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.) |
| ⊢ II ∈ Locally SConn | ||
| Theorem | iinllyconn 35259 | The unit interval is locally connected. (Contributed by Mario Carneiro, 6-Jul-2015.) |
| ⊢ II ∈ 𝑛-Locally Conn | ||
| Syntax | ccvm 35260 | Extend class notation with the class of covering maps. |
| class CovMap | ||
| Definition | df-cvm 35261* | 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 35262 | Lemma for covering maps. (Contributed by Mario Carneiro, 13-Feb-2015.) |
| ⊢ CovMap Fn (Top × Top) | ||
| Theorem | cvmscbv 35263* | Change bound variables in the set of even coverings. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ 𝑆 = (𝑎 ∈ 𝐽 ↦ {𝑏 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑏 = (◡𝐹 “ 𝑎) ∧ ∀𝑐 ∈ 𝑏 (∀𝑑 ∈ (𝑏 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑎))))}) | ||
| Theorem | iscvm 35264* | The property of being a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.) |
| ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) ↔ ((𝐶 ∈ Top ∧ 𝐽 ∈ Top ∧ 𝐹 ∈ (𝐶 Cn 𝐽)) ∧ ∀𝑥 ∈ 𝑋 ∃𝑘 ∈ 𝐽 (𝑥 ∈ 𝑘 ∧ (𝑆‘𝑘) ≠ ∅))) | ||
| Theorem | cvmtop1 35265 | Reverse closure for a covering map. (Contributed by Mario Carneiro, 11-Feb-2015.) |
| ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) | ||
| Theorem | cvmtop2 35266 | Reverse closure for a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.) |
| ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top) | ||
| Theorem | cvmcn 35267 | A covering map is a continuous function. (Contributed by Mario Carneiro, 13-Feb-2015.) |
| ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽)) | ||
| Theorem | cvmcov 35268* | 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 35269* | Reverse closure for an even covering. (Contributed by Mario Carneiro, 11-Feb-2015.) |
| ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑈 ∈ 𝐽) | ||
| Theorem | cvmsi 35270* | One direction of cvmsval 35271. (Contributed by Mario Carneiro, 13-Feb-2015.) |
| ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ (𝑇 ∈ (𝑆‘𝑈) → (𝑈 ∈ 𝐽 ∧ (𝑇 ⊆ 𝐶 ∧ 𝑇 ≠ ∅) ∧ (∪ 𝑇 = (◡𝐹 “ 𝑈) ∧ ∀𝑢 ∈ 𝑇 (∀𝑣 ∈ (𝑇 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑈)))))) | ||
| Theorem | cvmsval 35271* | 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 35272* | 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 35273* | An even covering is nonempty. (Contributed by Mario Carneiro, 11-Feb-2015.) |
| ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑇 ≠ ∅) | ||
| Theorem | cvmsuni 35274* | An even covering of 𝑈 has union equal to the preimage of 𝑈 by 𝐹. (Contributed by Mario Carneiro, 11-Feb-2015.) |
| ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ (𝑇 ∈ (𝑆‘𝑈) → ∪ 𝑇 = (◡𝐹 “ 𝑈)) | ||
| Theorem | cvmsdisj 35275* | An even covering of 𝑈 is a disjoint union. (Contributed by Mario Carneiro, 13-Feb-2015.) |
| ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ ((𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇) → (𝐴 = 𝐵 ∨ (𝐴 ∩ 𝐵) = ∅)) | ||
| Theorem | cvmshmeo 35276* | 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 35277* | 𝐹, 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 35278* | 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 35279* | An open subset of an evenly covered set is evenly covered. (Contributed by Mario Carneiro, 7-Jul-2015.) |
| ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) → ((𝑆‘𝑈) ≠ ∅ → (𝑆‘𝑉) ≠ ∅)) | ||
| Theorem | cvmcov2 35280* | The covering map property can be restricted to an open subset. (Contributed by Mario Carneiro, 7-Jul-2015.) |
| ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑥 ∈ 𝒫 𝑈(𝑃 ∈ 𝑥 ∧ (𝑆‘𝑥) ≠ ∅)) | ||
| Theorem | cvmseu 35281* | Every element in ∪ 𝑇 is a member of a unique element of 𝑇. (Contributed by Mario Carneiro, 14-Feb-2015.) |
| ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 ⇒ ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → ∃!𝑥 ∈ 𝑇 𝐴 ∈ 𝑥) | ||
| Theorem | cvmsiota 35282* | Identify the unique element of 𝑇 containing 𝐴. (Contributed by Mario Carneiro, 14-Feb-2015.) |
| ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑊 = (℩𝑥 ∈ 𝑇 𝐴 ∈ 𝑥) ⇒ ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → (𝑊 ∈ 𝑇 ∧ 𝐴 ∈ 𝑊)) | ||
| Theorem | cvmopnlem 35283* | Lemma for cvmopn 35285. (Contributed by Mario Carneiro, 7-May-2015.) |
| ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 ⇒ ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (𝐹 “ 𝐴) ∈ 𝐽) | ||
| Theorem | cvmfolem 35284* | Lemma for cvmfo 35305. (Contributed by Mario Carneiro, 13-Feb-2015.) |
| ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹:𝐵–onto→𝑋) | ||
| Theorem | cvmopn 35285 | A covering map is an open map. (Contributed by Mario Carneiro, 7-May-2015.) |
| ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (𝐹 “ 𝐴) ∈ 𝐽) | ||
| Theorem | cvmliftmolem1 35286* | Lemma for cvmliftmo 35289. (Contributed by Mario Carneiro, 10-Mar-2015.) |
| ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ Conn) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Conn) & ⊢ (𝜑 → 𝑂 ∈ 𝑌) & ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶)) & ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶)) & ⊢ (𝜑 → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁)) & ⊢ (𝜑 → (𝑀‘𝑂) = (𝑁‘𝑂)) & ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ∈ (𝑆‘𝑈)) & ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝑇) & ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ 𝑊)) & ⊢ ((𝜑 ∧ 𝜓) → (𝐾 ↾t 𝐼) ∈ Conn) & ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐼) & ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝐼) & ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝐼) & ⊢ ((𝜑 ∧ 𝜓) → (𝐹‘(𝑀‘𝑋)) ∈ 𝑈) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) → 𝑅 ∈ dom (𝑀 ∩ 𝑁))) | ||
| Theorem | cvmliftmolem2 35287* | Lemma for cvmliftmo 35289. (Contributed by Mario Carneiro, 10-Mar-2015.) |
| ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ Conn) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Conn) & ⊢ (𝜑 → 𝑂 ∈ 𝑌) & ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶)) & ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶)) & ⊢ (𝜑 → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁)) & ⊢ (𝜑 → (𝑀‘𝑂) = (𝑁‘𝑂)) & ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ (𝜑 → 𝑀 = 𝑁) | ||
| Theorem | cvmliftmoi 35288 | 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 35289* | 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 35290* | Lemma for cvmlift 35304. In cvmliftlem15 35303, 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 35291* | Lemma for cvmlift 35304. 𝑊 = [(𝑘 − 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 35292* | Lemma for cvmlift 35304. 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 35293* | Lemma for cvmlift 35304. 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 35294* | Lemma for cvmlift 35304. 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 35295* | Lemma for cvmlift 35304. Induction step for cvmliftlem7 35296. 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 35296* | Lemma for cvmlift 35304. Prove by induction that every 𝑄 function is well-defined (we can immediately follow this theorem with cvmliftlem6 35295 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 35297* | Lemma for cvmlift 35304. 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 𝐶)) | ||
| Theorem | cvmliftlem9 35298* | Lemma for cvmlift 35304. The 𝑄(𝑀) functions are defined on almost disjoint intervals, but they overlap at the edges. Here we show that at these points the 𝑄 functions agree on their common domain. (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) / 𝑁))) | ||
| Theorem | cvmliftlem10 35299* | Lemma for cvmlift 35304. The function 𝐾 is going to be our complete lifted path, formed by unioning together all the 𝑄 functions (each of which is defined on one segment [(𝑀 − 1) / 𝑁, 𝑀 / 𝑁] of the interval). Here we prove by induction that 𝐾 is a continuous function and a lift of 𝐺 by applying cvmliftlem6 35295, cvmliftlem7 35296 (to show it is a function and a lift), cvmliftlem8 35297 (to show it is continuous), and cvmliftlem9 35298 (to show that different 𝑄 functions agree on the intersection of their domains, so that the pasting lemma paste 23302 gives that 𝐾 is well-defined and continuous). (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...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))) ⇒ ⊢ (𝜑 → (𝐾 ∈ ((𝐿 ↾t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))) | ||
| Theorem | cvmliftlem11 35300* | Lemma for cvmlift 35304. (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...𝑁)(𝑄‘𝑘) ⇒ ⊢ (𝜑 → (𝐾 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = 𝐺)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |