Theorem List for Intuitionistic Logic Explorer - 12401-12500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | cnnei 12401* |
Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux,
3-Jan-2018.)
|
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪
𝐾
⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ∀𝑝 ∈ 𝑋 ∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑝)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑝})(𝐹 “ 𝑣) ⊆ 𝑤)) |
|
Theorem | cnconst2 12402 |
A constant function is continuous. (Contributed by Mario Carneiro,
19-Mar-2015.)
|
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐵 ∈ 𝑌) → (𝑋 × {𝐵}) ∈ (𝐽 Cn 𝐾)) |
|
Theorem | cnconst 12403 |
A constant function is continuous. (Contributed by FL, 15-Jan-2007.)
(Proof shortened by Mario Carneiro, 19-Mar-2015.)
|
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐵 ∈ 𝑌 ∧ 𝐹:𝑋⟶{𝐵})) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
|
Theorem | cnrest 12404 |
Continuity of a restriction from a subspace. (Contributed by Jeff
Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 21-Aug-2015.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾)) |
|
Theorem | cnrest2 12405 |
Equivalence of continuity in the parent topology and continuity in a
subspace. (Contributed by Jeff Hankins, 10-Jul-2009.) (Proof shortened
by Mario Carneiro, 21-Aug-2015.)
|
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵)))) |
|
Theorem | cnrest2r 12406 |
Equivalence of continuity in the parent topology and continuity in a
subspace. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario
Carneiro, 7-Jun-2014.)
|
⊢ (𝐾 ∈ Top → (𝐽 Cn (𝐾 ↾t 𝐵)) ⊆ (𝐽 Cn 𝐾)) |
|
Theorem | cnptopresti 12407 |
One direction of cnptoprest 12408 under the weaker condition that the point
is in the subset rather than the interior of the subset. (Contributed
by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon,
31-Mar-2023.)
|
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Top) ∧ (𝐴 ⊆ 𝑋 ∧ 𝑃 ∈ 𝐴 ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃))) → (𝐹 ↾ 𝐴) ∈ (((𝐽 ↾t 𝐴) CnP 𝐾)‘𝑃)) |
|
Theorem | cnptoprest 12408 |
Equivalence of continuity at a point and continuity of the restricted
function at a point. (Contributed by Mario Carneiro, 8-Aug-2014.)
(Revised by Jim Kingdon, 5-Apr-2023.)
|
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪
𝐾
⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹 ↾ 𝐴) ∈ (((𝐽 ↾t 𝐴) CnP 𝐾)‘𝑃))) |
|
Theorem | cnptoprest2 12409 |
Equivalence of point-continuity in the parent topology and
point-continuity in a subspace. (Contributed by Mario Carneiro,
9-Aug-2014.) (Revised by Jim Kingdon, 6-Apr-2023.)
|
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪
𝐾
⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ 𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃))) |
|
Theorem | cndis 12410 |
Every function is continuous when the domain is discrete. (Contributed
by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro,
21-Aug-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐽 ∈ (TopOn‘𝑋)) → (𝒫 𝐴 Cn 𝐽) = (𝑋 ↑𝑚 𝐴)) |
|
Theorem | cnpdis 12411 |
If 𝐴 is an isolated point in 𝑋 (or
equivalently, the singleton
{𝐴} is open in 𝑋), then every function is
continuous at
𝐴. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ {𝐴} ∈ 𝐽) → ((𝐽 CnP 𝐾)‘𝐴) = (𝑌 ↑𝑚 𝑋)) |
|
Theorem | lmfpm 12412 |
If 𝐹 converges, then 𝐹 is a
partial function. (Contributed by
Mario Carneiro, 23-Dec-2013.)
|
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ∈ (𝑋 ↑pm
ℂ)) |
|
Theorem | lmfss 12413 |
Inclusion of a function having a limit (used to ensure the limit
relation is a set, under our definition). (Contributed by NM,
7-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
|
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ⊆ (ℂ × 𝑋)) |
|
Theorem | lmcl 12414 |
Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by
Mario Carneiro, 23-Dec-2013.)
|
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ 𝑋) |
|
Theorem | lmss 12415 |
Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by
Mario Carneiro, 30-Dec-2013.)
|
⊢ 𝐾 = (𝐽 ↾t 𝑌)
& ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑌 ∈ 𝑉)
& ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑃 ∈ 𝑌)
& ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑌) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃)) |
|
Theorem | sslm 12416 |
A finer topology has fewer convergent sequences (but the sequences that
do converge, converge to the same value). (Contributed by Mario
Carneiro, 15-Sep-2015.)
|
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) →
(⇝𝑡‘𝐾) ⊆
(⇝𝑡‘𝐽)) |
|
Theorem | lmres 12417 |
A function converges iff its restriction to an upper integers set
converges. (Contributed by Mario Carneiro, 31-Dec-2013.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (𝑋 ↑pm
ℂ))
& ⊢ (𝜑 → 𝑀 ∈ ℤ)
⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ↾
(ℤ≥‘𝑀))(⇝𝑡‘𝐽)𝑃)) |
|
Theorem | lmff 12418* |
If 𝐹 converges, there is some upper
integer set on which 𝐹 is
a total function. (Contributed by Mario Carneiro, 31-Dec-2013.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ dom
(⇝𝑡‘𝐽)) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 (𝐹 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶𝑋) |
|
Theorem | lmtopcnp 12419 |
The image of a convergent sequence under a continuous map is
convergent to the image of the original point. (Contributed by Mario
Carneiro, 3-May-2014.) (Revised by Jim Kingdon, 6-Apr-2023.)
|
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)
& ⊢ (𝜑 → 𝐾 ∈ Top) & ⊢ (𝜑 → 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹)(⇝𝑡‘𝐾)(𝐺‘𝑃)) |
|
Theorem | lmcn 12420 |
The image of a convergent sequence under a continuous map is convergent
to the image of the original point. (Contributed by Mario Carneiro,
3-May-2014.)
|
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)
& ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹)(⇝𝑡‘𝐾)(𝐺‘𝑃)) |
|
7.1.8 Product topologies
|
|
Syntax | ctx 12421 |
Extend class notation with the binary topological product operation.
|
class ×t |
|
Definition | df-tx 12422* |
Define the binary topological product, which is homeomorphic to the
general topological product over a two element set, but is more
convenient to use. (Contributed by Jeff Madsen, 2-Sep-2009.)
|
⊢ ×t = (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)))) |
|
Theorem | txvalex 12423 |
Existence of the binary topological product. If 𝑅 and 𝑆 are
known to be topologies, see txtop 12429. (Contributed by Jim Kingdon,
3-Aug-2023.)
|
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝑅 ×t 𝑆) ∈ V) |
|
Theorem | txval 12424* |
Value of the binary topological product operation. (Contributed by Jeff
Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 30-Aug-2015.)
|
⊢ 𝐵 = ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦)) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝑅 ×t 𝑆) = (topGen‘𝐵)) |
|
Theorem | txuni2 12425* |
The underlying set of the product of two topologies. (Contributed by
Mario Carneiro, 31-Aug-2015.)
|
⊢ 𝐵 = ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦))
& ⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪
𝑆
⇒ ⊢ (𝑋 × 𝑌) = ∪ 𝐵 |
|
Theorem | txbasex 12426* |
The basis for the product topology is a set. (Contributed by Mario
Carneiro, 2-Sep-2015.)
|
⊢ 𝐵 = ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦)) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → 𝐵 ∈ V) |
|
Theorem | txbas 12427* |
The set of Cartesian products of elements from two topological bases is
a basis. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario
Carneiro, 31-Aug-2015.)
|
⊢ 𝐵 = ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦)) ⇒ ⊢ ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → 𝐵 ∈ TopBases) |
|
Theorem | eltx 12428* |
A set in a product is open iff each point is surrounded by an open
rectangle. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐾 ∈ 𝑊) → (𝑆 ∈ (𝐽 ×t 𝐾) ↔ ∀𝑝 ∈ 𝑆 ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐾 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝑆))) |
|
Theorem | txtop 12429 |
The product of two topologies is a topology. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top) |
|
Theorem | txtopi 12430 |
The product of two topologies is a topology. (Contributed by Jeff
Madsen, 15-Jun-2010.)
|
⊢ 𝑅 ∈ Top & ⊢ 𝑆 ∈
Top ⇒ ⊢ (𝑅 ×t 𝑆) ∈ Top |
|
Theorem | txtopon 12431 |
The underlying set of the product of two topologies. (Contributed by
Mario Carneiro, 22-Aug-2015.) (Revised by Mario Carneiro,
2-Sep-2015.)
|
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌))) |
|
Theorem | txuni 12432 |
The underlying set of the product of two topologies. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪
𝑆
⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆)) |
|
Theorem | txunii 12433 |
The underlying set of the product of two topologies. (Contributed by
Jeff Madsen, 15-Jun-2010.)
|
⊢ 𝑅 ∈ Top & ⊢ 𝑆 ∈ Top & ⊢ 𝑋 = ∪
𝑅 & ⊢ 𝑌 = ∪
𝑆
⇒ ⊢ (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆) |
|
Theorem | txopn 12434 |
The product of two open sets is open in the product topology.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴 × 𝐵) ∈ (𝑅 ×t 𝑆)) |
|
Theorem | txss12 12435 |
Subset property of the topological product. (Contributed by Mario
Carneiro, 2-Sep-2015.)
|
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)) → (𝐴 ×t 𝐶) ⊆ (𝐵 ×t 𝐷)) |
|
Theorem | txbasval 12436 |
It is sufficient to consider products of the bases for the topologies in
the topological product. (Contributed by Mario Carneiro,
25-Aug-2014.)
|
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ((topGen‘𝑅) ×t (topGen‘𝑆)) = (𝑅 ×t 𝑆)) |
|
Theorem | neitx 12437 |
The Cartesian product of two neighborhoods is a neighborhood in the
product topology. (Contributed by Thierry Arnoux, 13-Jan-2018.)
|
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪
𝐾
⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐴 × 𝐵) ∈ ((nei‘(𝐽 ×t 𝐾))‘(𝐶 × 𝐷))) |
|
Theorem | tx1cn 12438 |
Continuity of the first projection map of a topological product.
(Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario
Carneiro, 22-Aug-2015.)
|
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (1st ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑅)) |
|
Theorem | tx2cn 12439 |
Continuity of the second projection map of a topological product.
(Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario
Carneiro, 22-Aug-2015.)
|
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (2nd ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) |
|
Theorem | txcnp 12440* |
If two functions are continuous at 𝐷, then the ordered pair of them
is continuous at 𝐷 into the product topology.
(Contributed by Mario
Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → 𝐷 ∈ 𝑋)
& ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP 𝐾)‘𝐷)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ ((𝐽 CnP 𝐿)‘𝐷)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) ∈ ((𝐽 CnP (𝐾 ×t 𝐿))‘𝐷)) |
|
Theorem | upxp 12441* |
Universal property of the Cartesian product considered as a categorical
product in the category of sets. (Contributed by Jeff Madsen,
2-Sep-2009.) (Revised by Mario Carneiro, 27-Dec-2014.)
|
⊢ 𝑃 = (1st ↾ (𝐵 × 𝐶)) & ⊢ 𝑄 = (2nd ↾
(𝐵 × 𝐶))
⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → ∃!ℎ(ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) |
|
Theorem | txcnmpt 12442* |
A map into the product of two topological spaces is continuous if both
of its projections are continuous. (Contributed by Jeff Madsen,
2-Sep-2009.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
⊢ 𝑊 = ∪ 𝑈 & ⊢ 𝐻 = (𝑥 ∈ 𝑊 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ⇒ ⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐻 ∈ (𝑈 Cn (𝑅 ×t 𝑆))) |
|
Theorem | uptx 12443* |
Universal property of the binary topological product. (Contributed by
Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro,
22-Aug-2015.)
|
⊢ 𝑇 = (𝑅 ×t 𝑆)
& ⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪
𝑆 & ⊢ 𝑍 = (𝑋 × 𝑌)
& ⊢ 𝑃 = (1st ↾ 𝑍) & ⊢ 𝑄 = (2nd ↾
𝑍) ⇒ ⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃!ℎ ∈ (𝑈 Cn 𝑇)(𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) |
|
Theorem | txcn 12444 |
A map into the product of two topological spaces is continuous iff both
of its projections are continuous. (Contributed by Jeff Madsen,
2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
|
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪
𝑆 & ⊢ 𝑍 = (𝑋 × 𝑌)
& ⊢ 𝑊 = ∪ 𝑈 & ⊢ 𝑃 = (1st ↾
𝑍) & ⊢ 𝑄 = (2nd ↾
𝑍) ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ↔ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆)))) |
|
Theorem | txrest 12445 |
The subspace of a topological product space induced by a subset with a
Cartesian product representation is a topological product of the
subspaces induced by the subspaces of the terms of the products.
(Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario
Carneiro, 2-Sep-2015.)
|
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑅 ×t 𝑆) ↾t (𝐴 × 𝐵)) = ((𝑅 ↾t 𝐴) ×t (𝑆 ↾t 𝐵))) |
|
Theorem | txdis 12446 |
The topological product of discrete spaces is discrete. (Contributed by
Mario Carneiro, 14-Aug-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝒫 𝐴 ×t 𝒫 𝐵) = 𝒫 (𝐴 × 𝐵)) |
|
Theorem | txdis1cn 12447* |
A function is jointly continuous on a discrete left topology iff it is
continuous as a function of its right argument, for each fixed left
value. (Contributed by Mario Carneiro, 19-Sep-2015.)
|
⊢ (𝜑 → 𝑋 ∈ 𝑉)
& ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐾 ∈ Top) & ⊢ (𝜑 → 𝐹 Fn (𝑋 × 𝑌)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → 𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾)) |
|
Theorem | txlm 12448* |
Two sequences converge iff the sequence of their ordered pairs
converges. Proposition 14-2.6 of [Gleason] p. 230. (Contributed by
NM, 16-Jul-2007.) (Revised by Mario Carneiro, 5-May-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋)
& ⊢ (𝜑 → 𝐺:𝑍⟶𝑌)
& ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) ⇒ ⊢ (𝜑 → ((𝐹(⇝𝑡‘𝐽)𝑅 ∧ 𝐺(⇝𝑡‘𝐾)𝑆) ↔ 𝐻(⇝𝑡‘(𝐽 ×t 𝐾))〈𝑅, 𝑆〉)) |
|
Theorem | lmcn2 12449* |
The image of a convergent sequence under a continuous map is convergent
to the image of the original point. Binary operation version.
(Contributed by Mario Carneiro, 15-May-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋)
& ⊢ (𝜑 → 𝐺:𝑍⟶𝑌)
& ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑅)
& ⊢ (𝜑 → 𝐺(⇝𝑡‘𝐾)𝑆)
& ⊢ (𝜑 → 𝑂 ∈ ((𝐽 ×t 𝐾) Cn 𝑁)) & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)𝑂(𝐺‘𝑛))) ⇒ ⊢ (𝜑 → 𝐻(⇝𝑡‘𝑁)(𝑅𝑂𝑆)) |
|
7.1.9 Continuous function-builders
|
|
Theorem | cnmptid 12450* |
The identity function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑥) ∈ (𝐽 Cn 𝐽)) |
|
Theorem | cnmptc 12451* |
A constant function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝑃 ∈ 𝑌) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑃) ∈ (𝐽 Cn 𝐾)) |
|
Theorem | cnmpt11 12452* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 𝐵) ∈ (𝐾 Cn 𝐿)) & ⊢ (𝑦 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐶) ∈ (𝐽 Cn 𝐿)) |
|
Theorem | cnmpt11f 12453* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐹 ∈ (𝐾 Cn 𝐿)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐹‘𝐴)) ∈ (𝐽 Cn 𝐿)) |
|
Theorem | cnmpt1t 12454* |
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) ∈ (𝐽 Cn (𝐾 ×t 𝐿))) |
|
Theorem | cnmpt12f 12455* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐾 ×t 𝐿) Cn 𝑀)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝐽 Cn 𝑀)) |
|
Theorem | cnmpt12 12456* |
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 12-Jun-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → (𝑦 ∈ 𝑌, 𝑧 ∈ 𝑍 ↦ 𝐶) ∈ ((𝐾 ×t 𝐿) Cn 𝑀)) & ⊢ ((𝑦 = 𝐴 ∧ 𝑧 = 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐷) ∈ (𝐽 Cn 𝑀)) |
|
Theorem | cnmpt1st 12457* |
The projection onto the first coordinate is continuous. (Contributed by
Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑥) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) |
|
Theorem | cnmpt2nd 12458* |
The projection onto the second coordinate is continuous. (Contributed
by Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) |
|
Theorem | cnmpt2c 12459* |
A constant function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → 𝑃 ∈ 𝑍) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑃) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
|
Theorem | cnmpt21 12460* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → (𝑧 ∈ 𝑍 ↦ 𝐵) ∈ (𝐿 Cn 𝑀)) & ⊢ (𝑧 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) |
|
Theorem | cnmpt21f 12461* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) & ⊢ (𝜑 → 𝐹 ∈ (𝐿 Cn 𝑀)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐹‘𝐴)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) |
|
Theorem | cnmpt2t 12462* |
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈𝐴, 𝐵〉) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀))) |
|
Theorem | cnmpt22 12463* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑊)) & ⊢ (𝜑 → (𝑧 ∈ 𝑍, 𝑤 ∈ 𝑊 ↦ 𝐶) ∈ ((𝐿 ×t 𝑀) Cn 𝑁)) & ⊢ ((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐷) ∈ ((𝐽 ×t 𝐾) Cn 𝑁)) |
|
Theorem | cnmpt22f 12464* |
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐿 ×t 𝑀) Cn 𝑁)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴𝐹𝐵)) ∈ ((𝐽 ×t 𝐾) Cn 𝑁)) |
|
Theorem | cnmpt1res 12465* |
The restriction of a continuous function to a subset is continuous.
(Contributed by Mario Carneiro, 5-Jun-2014.)
|
⊢ 𝐾 = (𝐽 ↾t 𝑌)
& ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
& ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐿)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) |
|
Theorem | cnmpt2res 12466* |
The restriction of a continuous function to a subset is continuous.
(Contributed by Mario Carneiro, 6-Jun-2014.)
|
⊢ 𝐾 = (𝐽 ↾t 𝑌)
& ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
& ⊢ 𝑁 = (𝑀 ↾t 𝑊)
& ⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → 𝑊 ⊆ 𝑍)
& ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑍 ↦ 𝐴) ∈ ((𝐽 ×t 𝑀) Cn 𝐿)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑌, 𝑦 ∈ 𝑊 ↦ 𝐴) ∈ ((𝐾 ×t 𝑁) Cn 𝐿)) |
|
Theorem | cnmptcom 12467* |
The argument converse of a continuous function is continuous.
(Contributed by Mario Carneiro, 6-Jun-2014.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) ⇒ ⊢ (𝜑 → (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐾 ×t 𝐽) Cn 𝐿)) |
|
Theorem | imasnopn 12468 |
If a relation graph is open, then an image set of a singleton is also
open. Corollary of Proposition 4 of [BourbakiTop1] p. I.26.
(Contributed by Thierry Arnoux, 14-Jan-2018.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) ∈ 𝐾) |
|
7.1.10 Homeomorphisms
|
|
Syntax | chmeo 12469 |
Extend class notation with the class of all homeomorphisms.
|
class Homeo |
|
Definition | df-hmeo 12470* |
Function returning all the homeomorphisms from topology 𝑗 to
topology 𝑘. (Contributed by FL, 14-Feb-2007.)
|
⊢ Homeo = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (𝑗 Cn 𝑘) ∣ ◡𝑓 ∈ (𝑘 Cn 𝑗)}) |
|
Theorem | hmeofn 12471 |
The set of homeomorphisms is a function on topologies. (Contributed by
Mario Carneiro, 23-Aug-2015.)
|
⊢ Homeo Fn (Top × Top) |
|
Theorem | hmeofvalg 12472* |
The set of all the homeomorphisms between two topologies. (Contributed
by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽Homeo𝐾) = {𝑓 ∈ (𝐽 Cn 𝐾) ∣ ◡𝑓 ∈ (𝐾 Cn 𝐽)}) |
|
Theorem | ishmeo 12473 |
The predicate F is a homeomorphism between topology 𝐽 and topology
𝐾. Proposition of [BourbakiTop1] p. I.2. (Contributed by FL,
14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
⊢ (𝐹 ∈ (𝐽Homeo𝐾) ↔ (𝐹 ∈ (𝐽 Cn 𝐾) ∧ ◡𝐹 ∈ (𝐾 Cn 𝐽))) |
|
Theorem | hmeocn 12474 |
A homeomorphism is continuous. (Contributed by Mario Carneiro,
22-Aug-2015.)
|
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
|
Theorem | hmeocnvcn 12475 |
The converse of a homeomorphism is continuous. (Contributed by Mario
Carneiro, 22-Aug-2015.)
|
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → ◡𝐹 ∈ (𝐾 Cn 𝐽)) |
|
Theorem | hmeocnv 12476 |
The converse of a homeomorphism is a homeomorphism. (Contributed by FL,
5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → ◡𝐹 ∈ (𝐾Homeo𝐽)) |
|
Theorem | hmeof1o2 12477 |
A homeomorphism is a 1-1-onto mapping. (Contributed by Mario Carneiro,
22-Aug-2015.)
|
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽Homeo𝐾)) → 𝐹:𝑋–1-1-onto→𝑌) |
|
Theorem | hmeof1o 12478 |
A homeomorphism is a 1-1-onto mapping. (Contributed by FL, 5-Mar-2007.)
(Revised by Mario Carneiro, 30-May-2014.)
|
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪
𝐾
⇒ ⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹:𝑋–1-1-onto→𝑌) |
|
Theorem | hmeoima 12479 |
The image of an open set by a homeomorphism is an open set. (Contributed
by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ∈ 𝐽) → (𝐹 “ 𝐴) ∈ 𝐾) |
|
Theorem | hmeoopn 12480 |
Homeomorphisms preserve openness. (Contributed by Jeff Madsen,
2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ 𝐽 ↔ (𝐹 “ 𝐴) ∈ 𝐾)) |
|
Theorem | hmeocld 12481 |
Homeomorphisms preserve closedness. (Contributed by Jeff Madsen,
2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ (Clsd‘𝐽) ↔ (𝐹 “ 𝐴) ∈ (Clsd‘𝐾))) |
|
Theorem | hmeontr 12482 |
Homeomorphisms preserve interiors. (Contributed by Mario Carneiro,
25-Aug-2015.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → ((int‘𝐾)‘(𝐹 “ 𝐴)) = (𝐹 “ ((int‘𝐽)‘𝐴))) |
|
Theorem | hmeoimaf1o 12483* |
The function mapping open sets to their images under a homeomorphism is
a bijection of topologies. (Contributed by Mario Carneiro,
10-Sep-2015.)
|
⊢ 𝐺 = (𝑥 ∈ 𝐽 ↦ (𝐹 “ 𝑥)) ⇒ ⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐺:𝐽–1-1-onto→𝐾) |
|
Theorem | hmeores 12484 |
The restriction of a homeomorphism is a homeomorphism. (Contributed by
Mario Carneiro, 14-Sep-2014.) (Proof shortened by Mario Carneiro,
22-Aug-2015.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌)Homeo(𝐾 ↾t (𝐹 “ 𝑌)))) |
|
Theorem | hmeoco 12485 |
The composite of two homeomorphisms is a homeomorphism. (Contributed by
FL, 9-Mar-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
|
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐺 ∈ (𝐾Homeo𝐿)) → (𝐺 ∘ 𝐹) ∈ (𝐽Homeo𝐿)) |
|
Theorem | idhmeo 12486 |
The identity function is a homeomorphism. (Contributed by FL,
14-Feb-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
|
⊢ (𝐽 ∈ (TopOn‘𝑋) → ( I ↾ 𝑋) ∈ (𝐽Homeo𝐽)) |
|
Theorem | hmeocnvb 12487 |
The converse of a homeomorphism is a homeomorphism. (Contributed by FL,
5-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
|
⊢ (Rel 𝐹 → (◡𝐹 ∈ (𝐽Homeo𝐾) ↔ 𝐹 ∈ (𝐾Homeo𝐽))) |
|
Theorem | txhmeo 12488* |
Lift a pair of homeomorphisms on the factors to a homeomorphism of
product topologies. (Contributed by Mario Carneiro, 2-Sep-2015.)
|
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪
𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐽Homeo𝐿)) & ⊢ (𝜑 → 𝐺 ∈ (𝐾Homeo𝑀)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) ∈ ((𝐽 ×t 𝐾)Homeo(𝐿 ×t 𝑀))) |
|
Theorem | txswaphmeolem 12489* |
Show inverse for the "swap components" operation on a Cartesian
product.
(Contributed by Mario Carneiro, 21-Mar-2015.)
|
⊢ ((𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 〈𝑥, 𝑦〉) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈𝑦, 𝑥〉)) = ( I ↾ (𝑋 × 𝑌)) |
|
Theorem | txswaphmeo 12490* |
There is a homeomorphism from 𝑋 × 𝑌 to 𝑌 × 𝑋. (Contributed
by Mario Carneiro, 21-Mar-2015.)
|
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈𝑦, 𝑥〉) ∈ ((𝐽 ×t 𝐾)Homeo(𝐾 ×t 𝐽))) |
|
7.2 Metric spaces
|
|
7.2.1 Pseudometric spaces
|
|
Theorem | psmetrel 12491 |
The class of pseudometrics is a relation. (Contributed by Jim Kingdon,
24-Apr-2023.)
|
⊢ Rel PsMet |
|
Theorem | ispsmet 12492* |
Express the predicate "𝐷 is a pseudometric."
(Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
⊢ (𝑋 ∈ 𝑉 → (𝐷 ∈ (PsMet‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ* ∧
∀𝑥 ∈ 𝑋 ((𝑥𝐷𝑥) = 0 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))))) |
|
Theorem | psmetdmdm 12493 |
Recover the base set from a pseudometric. (Contributed by Thierry
Arnoux, 7-Feb-2018.)
|
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 = dom dom 𝐷) |
|
Theorem | psmetf 12494 |
The distance function of a pseudometric as a function. (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
|
Theorem | psmetcl 12495 |
Closure of the distance function of a pseudometric space. (Contributed
by Thierry Arnoux, 7-Feb-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈
ℝ*) |
|
Theorem | psmet0 12496 |
The distance function of a pseudometric space is zero if its arguments
are equal. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 0) |
|
Theorem | psmettri2 12497 |
Triangle inequality for the distance function of a pseudometric.
(Contributed by Thierry Arnoux, 11-Feb-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵))) |
|
Theorem | psmetsym 12498 |
The distance function of a pseudometric is symmetrical. (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) |
|
Theorem | psmettri 12499 |
Triangle inequality for the distance function of a pseudometric space.
(Contributed by Thierry Arnoux, 11-Feb-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐶𝐷𝐵))) |
|
Theorem | psmetge0 12500 |
The distance function of a pseudometric space is nonnegative.
(Contributed by Thierry Arnoux, 7-Feb-2018.) (Revised by Jim Kingdon,
19-Apr-2023.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵)) |