Beginning of Section Topology
Proof: Load proof Proof not loaded.
Definition. We define
open_in to be
λX T U ⇒ topology_on X T ∧ U ∈ T of type
set → set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
finer_than to be
λT' T ⇒ T ⊆ T' of type
set → set → prop .
Definition. We define
coarser_than to be
λT' T ⇒ T' ⊆ T of type
set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
open_set_family to be
λ_ T ⇒ T of type
set → set → set .
Definition. We define
open_set to be
open_in of type
set → set → set → prop .
Definition. We define
basis_on to be
λX B ⇒ B ⊆ 𝒫 X ∧ (∀x ∈ X , ∃b ∈ B , x ∈ b ) ∧ (∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) of type
set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
R to be
real of type
set .
Definition. We define
Q to be
rational of type
set .
Definition. We define
Rlt to be
λa b ⇒ a ∈ R ∧ b ∈ R ∧ a < b of type
set → set → prop .
Definition. We define
Rle to be
λa b ⇒ a ∈ R ∧ b ∈ R ∧ ¬ (Rlt b a ) of type
set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
R2_xcoord to be
λp ⇒ p 0 of type
set → set .
Definition. We define
R2_ycoord to be
λp ⇒ p 1 of type
set → set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
subbasis_on to be
λX S ⇒ S ⊆ 𝒫 X ∧ ⋃ S = X of type
set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
a_elt to be
Empty of type
set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
ex13_4b_smallest_largest )
∀X Fam : set , (∀T ∈ Fam , topology_on X T ) → ∃Tmin, topology_on X Tmin ∧ (∀T ∈ Fam , T ⊆ Tmin ) ∧ (∀T', topology_on X T' ∧ (∀T ∈ Fam , T ⊆ T' ) → Tmin ⊆ T' ) ∧ ∃Tmax, topology_on X Tmax ∧ (∀T ∈ Fam , Tmax ⊆ T ) ∧ (∀T', topology_on X T' ∧ (∀T ∈ Fam , T' ⊆ T ) → T' ⊆ Tmax )
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
tag_topology .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
Zplus to be
ω ∖ { 0 } of type
set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
and7E )
∀A B C D E F G : prop , A ∧ B ∧ C ∧ D ∧ E ∧ F ∧ G → ∀p : prop , (A → B → C → D → E → F → G → p ) → p
Proof: Load proof Proof not loaded.
Theorem. (
and4E )
∀A B C D : prop , A ∧ B ∧ C ∧ D → ∀p : prop , (A → B → C → D → p ) → p
Proof: Load proof Proof not loaded.
Theorem. (
and5E )
∀A B C D E : prop , A ∧ B ∧ C ∧ D ∧ E → ∀p : prop , (A → B → C → D → E → p ) → p
Proof: Load proof Proof not loaded.
Theorem. (
and6E )
∀A B C D E F : prop , A ∧ B ∧ C ∧ D ∧ E ∧ F → ∀p : prop , (A → B → C → D → E → F → p ) → p
Proof: Load proof Proof not loaded.
Theorem. (
mem_eqR )
∀x A B : set , A = B → x ∈ A → x ∈ B
Proof: Load proof Proof not loaded.
Theorem. (
mem_eqL )
∀x A B : set , A = B → x ∈ B → x ∈ A
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
apply_fun to be
λf x ⇒ Eps_i (λy ⇒ (x ,y ) ∈ f ) of type
set → set → set .
Definition. We define
function_on to be
λf X Y ⇒ ∀x : set , x ∈ X → apply_fun f x ∈ Y of type
set → set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
functional_graph to be
λf ⇒ ∀x y1 y2 : set , (x ,y1 ) ∈ f → (x ,y2 ) ∈ f → y1 = y2 of type
set → prop .
Definition. We define
graph_domain_subset to be
λf X ⇒ ∀x y : set , (x ,y ) ∈ f → x ∈ X of type
set → set → prop .
Definition. We define
graph_range_subset to be
λf Y ⇒ ∀x y : set , (x ,y ) ∈ f → y ∈ Y of type
set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
graph to be
λA g ⇒ { (a ,g a ) | a ∈ A } of type
set → (set → set ) → set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
const_fun to be
λA x ⇒ { (a ,x ) | a ∈ A } of type
set → set → set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
const_family to be
λI X ⇒ { (i ,X ) | i ∈ I } of type
set → set → set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
interior_of to be
λX T A ⇒ { x ∈ X | ∃U : set , U ∈ T ∧ x ∈ U ∧ U ⊆ A } of type
set → set → set → set .
Definition. We define
closure_of to be
λX T A ⇒ { x ∈ X | ∀U : set , U ∈ T → x ∈ U → U ∩ A ≠ Empty } of type
set → set → set → set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
ordsq_p01 to be
(0 ,1 ) of type
set .
Definition. We define
ordsq_p10 to be
(1 ,0 ) of type
set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
continuous_construction_rules )
∀X Tx Y Ty Z Tz : set , topology_on X Tx → topology_on Y Ty → topology_on Z Tz → (∀y0 : set , y0 ∈ Y → continuous_map X Tx Y Ty (const_fun X y0 ) ) ∧ (∀A : set , A ⊆ X → continuous_map A (subspace_topology X Tx A ) X Tx { (y ,y ) | y ∈ A } ) ∧ (∀f g : set , continuous_map X Tx Y Ty f → continuous_map Y Ty Z Tz g → continuous_map X Tx Z Tz (compose_fun X f g ) ) ∧ (∀f A : set , A ⊆ X → continuous_map X Tx Y Ty f → continuous_map A (subspace_topology X Tx A ) Y Ty f ) ∧ ((∀f Z0 : set , continuous_map X Tx Y Ty f → Z0 ⊆ Y → (∀x : set , x ∈ X → apply_fun f x ∈ Z0 ) → continuous_map X Tx Z0 (subspace_topology Y Ty Z0 ) f ) ∧ (∀f Z0 Tz0 : set , continuous_map X Tx Y Ty f → Y ⊆ Z0 → topology_on Z0 Tz0 → Ty = subspace_topology Z0 Tz0 Y → continuous_map X Tx Z0 Tz0 f ) ) ∧ (∀f : set , (∃UFam : set , UFam ⊆ Tx ∧ ⋃ UFam = X ∧ (∀U : set , U ∈ UFam → continuous_map U (subspace_topology X Tx U ) Y Ty f ) ) → continuous_map X Tx Y Ty f )
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
metric_on to be
λX d ⇒ function_on d (setprod X X ) R ∧ (∀x y : set , x ∈ X → y ∈ X → apply_fun d (x ,y ) = apply_fun d (y ,x ) ) ∧ (∀x : set , x ∈ X → apply_fun d (x ,x ) = 0 ) ∧ (∀x y : set , x ∈ X → y ∈ X → ¬ (Rlt (apply_fun d (x ,y ) ) 0 ) ∧ (apply_fun d (x ,y ) = 0 → x = y ) ) ∧ (∀x y z : set , x ∈ X → y ∈ X → z ∈ X → ¬ (Rlt (add_SNo (apply_fun d (x ,y ) ) (apply_fun d (y ,z ) ) ) (apply_fun d (x ,z ) ) ) ) of type
set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
R_upper_bound to be
λA u ⇒ u ∈ R ∧ ∀a : set , a ∈ A → a ∈ R → Rle a u of type
set → set → prop .
Definition. We define
R_lub to be
λA l ⇒ l ∈ R ∧ (∀a : set , a ∈ A → a ∈ R → Rle a l ) ∧ (∀u : set , u ∈ R → (∀a : set , a ∈ A → a ∈ R → Rle a u ) → Rle l u ) of type
set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
not_imp )
∀A B : prop , ¬ (A → B ) → A ∧ ¬ B
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
covers to be
λX U ⇒ ∀x : set , x ∈ X → ∃u : set , u ∈ U ∧ x ∈ u of type
set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
Abs to be
abs_SNo of type
set → set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
relation_on to be
λle J ⇒ ∀a b : set , (a ,b ) ∈ le → a ∈ J ∧ b ∈ J of type
set → set → prop .
Definition. We define
partial_order_on to be
λJ le ⇒ relation_on le J ∧ (∀a : set , a ∈ J → (a ,a ) ∈ le ) ∧ (∀a b : set , a ∈ J → b ∈ J → (a ,b ) ∈ le → (b ,a ) ∈ le → a = b ) ∧ (∀a b c : set , a ∈ J → b ∈ J → c ∈ J → (a ,b ) ∈ le → (b ,c ) ∈ le → (a ,c ) ∈ le ) of type
set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
net_pack to be
λJ le net ⇒ (J ,(le ,net ) ) of type
set → set → set → set .
Definition. We define
net_pack_le to be
λN ⇒ (N 1 ) 0 of type
set → set .
Definition. We define
net_pack_fun to be
λN ⇒ (N 1 ) 1 of type
set → set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Beginning of Section PropN2
Variable P1 P2 P3 P4 P5 P6 P7 P8 P9 P10 P11 P12 P13 P14 : prop
Theorem. (
and8I )
P1 → P2 → P3 → P4 → P5 → P6 → P7 → P8 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7 ∧ P8
Proof: Load proof Proof not loaded.
Theorem. (
and9I )
P1 → P2 → P3 → P4 → P5 → P6 → P7 → P8 → P9 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7 ∧ P8 ∧ P9
Proof: Load proof Proof not loaded.
Theorem. (
and10I )
P1 → P2 → P3 → P4 → P5 → P6 → P7 → P8 → P9 → P10 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7 ∧ P8 ∧ P9 ∧ P10
Proof: Load proof Proof not loaded.
Theorem. (
and11I )
P1 → P2 → P3 → P4 → P5 → P6 → P7 → P8 → P9 → P10 → P11 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7 ∧ P8 ∧ P9 ∧ P10 ∧ P11
Proof: Load proof Proof not loaded.
Theorem. (
and12I )
P1 → P2 → P3 → P4 → P5 → P6 → P7 → P8 → P9 → P10 → P11 → P12 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7 ∧ P8 ∧ P9 ∧ P10 ∧ P11 ∧ P12
Proof: Load proof Proof not loaded.
Theorem. (
and13I )
P1 → P2 → P3 → P4 → P5 → P6 → P7 → P8 → P9 → P10 → P11 → P12 → P13 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7 ∧ P8 ∧ P9 ∧ P10 ∧ P11 ∧ P12 ∧ P13
Proof: Load proof Proof not loaded.
Theorem. (
and14I )
P1 → P2 → P3 → P4 → P5 → P6 → P7 → P8 → P9 → P10 → P11 → P12 → P13 → P14 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7 ∧ P8 ∧ P9 ∧ P10 ∧ P11 ∧ P12 ∧ P13 ∧ P14
Proof: Load proof Proof not loaded.
End of Section PropN2
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
subnet_preserves_convergence_witnessed )
∀X Tx net sub x J leJ K leK phi : set , topology_on X Tx → directed_set J leJ → directed_set K leK → total_function_on net J X → functional_graph net → graph_domain_subset net J → total_function_on sub K X → functional_graph sub → graph_domain_subset sub K → total_function_on phi K J → functional_graph phi → graph_domain_subset phi K → (∀i j : set , i ∈ K → j ∈ K → (i ,j ) ∈ leK → (apply_fun phi i ,apply_fun phi j ) ∈ leJ ) → (∀j : set , j ∈ J → ∃k : set , k ∈ K ∧ (j ,apply_fun phi k ) ∈ leJ ) → (∀k : set , k ∈ K → apply_fun sub k = apply_fun net (apply_fun phi k ) ) → x ∈ X → (∀U : set , U ∈ Tx → x ∈ U → ∃j0 : set , j0 ∈ J ∧ ∀j : set , j ∈ J → (j0 ,j ) ∈ leJ → apply_fun net j ∈ U ) → net_converges X Tx sub x
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
net_points_in to be
λA net J ⇒ ∀j : set , j ∈ J → apply_fun net j ∈ A of type
set → set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
open_cover to be
λX Tx U ⇒ (∀u : set , u ∈ U → u ∈ Tx ) ∧ covers X U of type
set → set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
discrete_subspace to be
λX Tx A ⇒ A ⊆ X ∧ (∀a : set , a ∈ A → ∃U : set , U ∈ Tx ∧ U ∩ A = { a } ) of type
set → set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
dense_in to be
λA X Tx ⇒ closure_of X Tx A = X of type
set → set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
R_K to be
R of type
set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
partition_of_unity_dominated to be
λX Tx U ⇒ topology_on X Tx ∧ open_cover X Tx U ∧ ∃P : set , P ⊆ function_space X R ∧ (∀f : set , f ∈ P → continuous_map X Tx R R_standard_topology f ) ∧ (∀f x : set , f ∈ P → x ∈ X → apply_fun f x ∈ unit_interval ) ∧ (∀f : set , f ∈ P → ∃u : set , u ∈ U ∧ support_of X Tx f ⊆ u ) ∧ (∀x : set , x ∈ X → ∃N : set , N ∈ Tx ∧ x ∈ N ∧ ∃F0 : set , finite F0 ∧ F0 ⊆ P ∧ ∀f : set , f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0 ) ∧ (∀x : set , x ∈ X → ∃F : set , finite F ∧ F ⊆ P ∧ (∀f : set , f ∈ P → apply_fun f x ≠ 0 → f ∈ F ) ∧ ∃n : set , n ∈ ω ∧ ∃e : set , bijection n F e ∧ ∃p : set , function_on p (ordsucc n ) R ∧ apply_fun p Empty = 0 ∧ (∀k : set , k ∈ n → apply_fun p (ordsucc k ) = add_SNo (apply_fun p k ) (apply_fun (apply_fun e k ) x ) ) ∧ apply_fun p n = 1 ) of type
set → set → set → prop .
Definition. We define
partition_of_unity_family to be
λX Tx U P ⇒ P ⊆ function_space X R ∧ (∀f : set , f ∈ P → continuous_map X Tx R R_standard_topology f ) ∧ (∀f x : set , f ∈ P → x ∈ X → apply_fun f x ∈ unit_interval ) ∧ (∀f : set , f ∈ P → ∃u : set , u ∈ U ∧ support_of X Tx f ⊆ u ) ∧ (∀x : set , x ∈ X → ∃N : set , N ∈ Tx ∧ x ∈ N ∧ ∃F0 : set , finite F0 ∧ F0 ⊆ P ∧ ∀f : set , f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0 ) ∧ (∀x : set , x ∈ X → ∃F : set , finite F ∧ F ⊆ P ∧ (∀f : set , f ∈ P → apply_fun f x ≠ 0 → f ∈ F ) ∧ ∃n : set , n ∈ ω ∧ ∃e : set , bijection n F e ∧ ∃p : set , function_on p (ordsucc n ) R ∧ apply_fun p Empty = 0 ∧ (∀k : set , k ∈ n → apply_fun p (ordsucc k ) = add_SNo (apply_fun p k ) (apply_fun (apply_fun e k ) x ) ) ∧ apply_fun p n = 1 ) of type
set → set → set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
locally_finite_supports_pointwise_sum_witness )
∀X Tx P : set , topology_on X Tx → P ⊆ function_space X R → (∀f x : set , f ∈ P → x ∈ X → apply_fun f x ∈ unit_interval ) → (∀x : set , x ∈ X → ∃N : set , N ∈ Tx ∧ x ∈ N ∧ ∃F0 : set , finite F0 ∧ F0 ⊆ P ∧ ∀f : set , f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0 ) → ∀x : set , x ∈ X → ∃F : set , finite F ∧ F ⊆ P ∧ (∀f : set , f ∈ P → apply_fun f x ≠ 0 → f ∈ F ) ∧ ∃n : set , n ∈ ω ∧ ∃e : set , bijection n F e ∧ ∃p : set , function_on p (ordsucc n ) R ∧ apply_fun p Empty = 0 ∧ (∀k : set , k ∈ n → apply_fun p (ordsucc k ) = add_SNo (apply_fun p k ) (apply_fun (apply_fun e k ) x ) )
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
partition_of_unity_dominated_ex_family )
∀X Tx U : set , partition_of_unity_dominated X Tx U → ∃P : set , P ⊆ function_space X R ∧ (∀f : set , f ∈ P → continuous_map X Tx R R_standard_topology f ) ∧ (∀f x : set , f ∈ P → x ∈ X → apply_fun f x ∈ unit_interval ) ∧ (∀f : set , f ∈ P → ∃u : set , u ∈ U ∧ support_of X Tx f ⊆ u ) ∧ (∀x : set , x ∈ X → ∃N : set , N ∈ Tx ∧ x ∈ N ∧ ∃F0 : set , finite F0 ∧ F0 ⊆ P ∧ ∀f : set , f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0 ) ∧ (∀x : set , x ∈ X → ∃F : set , finite F ∧ F ⊆ P ∧ (∀f : set , f ∈ P → apply_fun f x ≠ 0 → f ∈ F ) ∧ ∃n : set , n ∈ ω ∧ ∃e : set , bijection n F e ∧ ∃p : set , function_on p (ordsucc n ) R ∧ apply_fun p Empty = 0 ∧ (∀k : set , k ∈ n → apply_fun p (ordsucc k ) = add_SNo (apply_fun p k ) (apply_fun (apply_fun e k ) x ) ) ∧ apply_fun p n = 1 )
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
partition_of_unity_dominated_supports_locally_finite )
∀X Tx U : set , partition_of_unity_dominated X Tx U → ∃P : set , P ⊆ function_space X R ∧ (∀f : set , f ∈ P → continuous_map X Tx R R_standard_topology f ) ∧ (∀f x : set , f ∈ P → x ∈ X → apply_fun f x ∈ unit_interval ) ∧ (∀f : set , f ∈ P → ∃u : set , u ∈ U ∧ support_of X Tx f ⊆ u ) ∧ (∀x : set , x ∈ X → ∃N : set , N ∈ Tx ∧ x ∈ N ∧ ∃F0 : set , finite F0 ∧ F0 ⊆ P ∧ ∀f : set , f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0 )
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
point_finite_cover_has_max_index )
∀X W I : set , ∀idx pickW : set → set , ordinal I → covers X W → (∀x : set , x ∈ X → ∃S : set , finite S ∧ S ⊆ W ∧ ∀A : set , A ∈ W → x ∈ A → A ∈ S ) → (∀w : set , w ∈ W → idx w ∈ I ) → (∀i : set , i ∈ I → pickW i ∈ W ∧ idx (pickW i ) = i ) → (∀w : set , w ∈ W → pickW (idx w ) = w ) → ∀x : set , x ∈ X → ∃imax : set , imax ∈ I ∧ x ∈ pickW imax ∧ ∀j : set , j ∈ I → imax ∈ j → x ∉ pickW j
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
refine_of to be
λV U ⇒ ∀v : set , v ∈ V → ∃u : set , u ∈ U ∧ v ⊆ u of type
set → set → prop .
Theorem. (
locally_finite_bump_cover_normalizes_to_partition_of_unity_dominated )
∀X Tx U V P : set , topology_on X Tx → open_cover X Tx U → open_cover X Tx V → locally_finite_family X Tx V → refine_of V U → P ⊆ function_space X R ∧ (∀f : set , f ∈ P → continuous_map X Tx R R_standard_topology f ) ∧ (∀f x : set , f ∈ P → x ∈ X → apply_fun f x ∈ unit_interval ) ∧ (∀f : set , f ∈ P → ∃u : set , u ∈ U ∧ support_of X Tx f ⊆ u ) ∧ (∀x : set , x ∈ X → ∃f : set , f ∈ P ∧ apply_fun f x = 1 ) ∧ (∀x : set , x ∈ X → ∃N : set , N ∈ Tx ∧ x ∈ N ∧ ∃F0 : set , finite F0 ∧ F0 ⊆ P ∧ ∀f : set , f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0 ) → partition_of_unity_dominated X Tx U
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
paracompact_Hausdorff_bump_cover_dominated )
∀X Tx U : set , paracompact_space X Tx → Hausdorff_space X Tx → open_cover X Tx U → ∃V P : set , open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U ∧ P ⊆ function_space X R ∧ (∀f : set , f ∈ P → continuous_map X Tx R R_standard_topology f ) ∧ (∀f x : set , f ∈ P → x ∈ X → apply_fun f x ∈ unit_interval ) ∧ (∀f : set , f ∈ P → ∃u : set , u ∈ U ∧ support_of X Tx f ⊆ u ) ∧ (∀x : set , x ∈ X → ∃f : set , f ∈ P ∧ apply_fun f x = 1 ) ∧ (∀x : set , x ∈ X → ∃N : set , N ∈ Tx ∧ x ∈ N ∧ ∃F0 : set , finite F0 ∧ F0 ⊆ P ∧ ∀f : set , f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0 )
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
U_eps to be
λX Tx Y d fn eps ⇒ ⋃ { interior_of X Tx (A_N_eps X Y d fn N eps ) | N ∈ ω } of type
set → set → set → set → set → set → set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
refines_cover to be
λB A ⇒ ∀U : set , U ∈ B → ∃V : set , V ∈ A ∧ U ⊆ V of type
set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
two to be
2 of type
set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
R3_xcoord to be
λp ⇒ p 0 of type
set → set .
Definition. We define
R3_ycoord to be
λp ⇒ p 1 of type
set → set .
Definition. We define
R3_zcoord to be
λp ⇒ p 2 of type
set → set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
topological_group to be
λG Tg ⇒ T1_space G Tg ∧ ∃mult inv e : set , function_on mult (setprod G G ) G ∧ function_on inv G G ∧ e ∈ G ∧ (∀x y z : set , x ∈ G → y ∈ G → z ∈ G → apply_fun mult (apply_fun mult (x ,y ) ,z ) = apply_fun mult (x ,apply_fun mult (y ,z ) ) ) ∧ (∀x : set , x ∈ G → apply_fun mult (e ,x ) = x ∧ apply_fun mult (x ,e ) = x ) ∧ (∀x : set , x ∈ G → apply_fun mult (x ,apply_fun inv x ) = e ∧ apply_fun mult (apply_fun inv x ,x ) = e ) ∧ continuous_map (setprod G G ) (product_topology G Tg G Tg ) G Tg mult ∧ continuous_map G Tg G Tg inv of type
set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
linear_continuum to be
λX Tx ⇒ simply_ordered_set X ∧ Tx = order_topology X ∧ (∃x y : set , x ∈ X ∧ y ∈ X ∧ x ≠ y ) ∧ (∀x y : set , x ∈ X → y ∈ X → order_rel X x y → ∃z : set , z ∈ X ∧ order_rel X x z ∧ order_rel X z y ) ∧ (∀A : set , A ⊆ X → A ≠ Empty → (∃upper : set , upper ∈ X ∧ ∀a : set , a ∈ A → order_rel X a upper ∨ a = upper ) → ∃lub : set , lub ∈ X ∧ (∀a : set , a ∈ A → order_rel X a lub ∨ a = lub ) ∧ (∀bound : set , bound ∈ X → (∀a : set , a ∈ A → order_rel X a bound ∨ a = bound ) → order_rel X lub bound ∨ lub = bound ) ) of type
set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
ex32_2_factors_inherit_separation )
∀Idx Fam : set , (∀i : set , i ∈ Idx → ∃Xi Txi : set , apply_fun Fam i = (Xi ,Txi ) ∧ Xi ≠ Empty ) → ((Hausdorff_space (product_space Idx Fam ) (product_topology_full Idx Fam ) → ∀i : set , i ∈ Idx → ∃Xi Txi : set , apply_fun Fam i = (Xi ,Txi ) ∧ Hausdorff_space Xi Txi ) ∧ (regular_space (product_space Idx Fam ) (product_topology_full Idx Fam ) → ∀i : set , i ∈ Idx → ∃Xi Txi : set , apply_fun Fam i = (Xi ,Txi ) ∧ regular_space Xi Txi ) ∧ (normal_space (product_space Idx Fam ) (product_topology_full Idx Fam ) → ∀i : set , i ∈ Idx → ∃Xi Txi : set , apply_fun Fam i = (Xi ,Txi ) ∧ normal_space Xi Txi ) )
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
image_of_map to be
λX Tx Y Ty f ⇒ image_of f X of type
set → set → set → set → set → set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.