Movatterモバイル変換

[0]ホーム

23127

Description:Define a function on twotopologies whose value is the set of continuous mappings from the first topology to the second. Based on definition of continuous function in [Munkres] p.102. Seeiscn 23135 for the predicate form. (Contributed by NM, 17-Oct-2006.)

**Assertion**
Ref	Expression
	⊢ Cn =(𝑗 ∈ Top,𝑘 ∈ Top ↦ {𝑓 ∈ (𝑘↑_m𝑗) ∣ ∀𝑦 ∈𝑘 (𝑓 “𝑦) ∈𝑗})

Distinct variable group: 𝑗,𝑘,𝑓,𝑦

**Detailed syntax breakdown of Definition**
Step	Hyp	Ref	Expression
1		ccn 23124	. 2classCn
2		vj	. . 3setvar𝑗
3		vk	. . 3setvar𝑘
4		ctop 22793	. . 3classTop
5		vf	. . . . . . . . 9setvar𝑓
6	5	cv 1539	. . . . . . . 8class𝑓
7	6	ccnv 5645	. . . . . . 7class𝑓
8		vy	. . . . . . . 8setvar𝑦
9	8	cv 1539	. . . . . . 7class𝑦
10	7,9	cima 5649	. . . . . 6class(𝑓 “𝑦)
11	2	cv 1539	. . . . . 6class𝑗
12	10,11	wcel 2109	. . . . 5wff(𝑓 “𝑦) ∈𝑗
13	3	cv 1539	. . . . 5class𝑘
14	12,8,13	wral 3046	. . . 4wff∀𝑦 ∈𝑘 (𝑓 “𝑦) ∈𝑗
15	13	cuni 4879	. . . . 5class𝑘
16	11	cuni 4879	. . . . 5class𝑗
17		cmap 8810	. . . . 5class↑_m
18	15,16,17	co 7394	. . . 4class(𝑘↑_m𝑗)
19	14,5,18	crab 3411	. . 3class{𝑓 ∈ (𝑘↑_m𝑗) ∣ ∀𝑦 ∈𝑘 (𝑓 “𝑦) ∈𝑗}
20	2,3,4,4,19	cmpo 7396	. 2class(𝑗 ∈ Top,𝑘 ∈ Top ↦ {𝑓 ∈ (𝑘 ↑_m𝑗)∣ ∀𝑦 ∈𝑘 (𝑓 “𝑦) ∈𝑗})
21	1,20	wceq 1540	1wff Cn =(𝑗 ∈ Top,𝑘 ∈ Top ↦ {𝑓 ∈ (𝑘↑_m𝑗) ∣ ∀𝑦 ∈𝑘 (𝑓 “𝑦) ∈𝑗})

[8]ページ先頭