- SIGMA_PROPERTY_DISJOINT_LEMMA
-
|- ∀sp a p.
algebra (sp,a) ∧ a ⊆ p ∧ closed_cdi (sp,p) ⇒ subsets (sigma sp a) ⊆ p
- SIGMA_PROPERTY_DISJOINT_LEMMA2
-
|- ∀a.
algebra a ⇒
∀s t.
s ∈ subsets (smallest_closed_cdi a) ∧
t ∈ subsets (smallest_closed_cdi a) ⇒
s ∩ t ∈ subsets (smallest_closed_cdi a)
- SIGMA_PROPERTY_DISJOINT_LEMMA1
-
|- ∀a.
algebra a ⇒
∀s t.
s ∈ subsets a ∧ t ∈ subsets (smallest_closed_cdi a) ⇒
s ∩ t ∈ subsets (smallest_closed_cdi a)
- CLOSED_CDI_INCREASING
-
|- ∀p f.
closed_cdi p ∧ f ∈ (𝕌(:num) -> subsets p) ∧ (f 0 = ∅) ∧
(∀n. f n ⊆ f (SUC n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets p
- CLOSED_CDI_DISJOINT
-
|- ∀p f.
closed_cdi p ∧ f ∈ (𝕌(:num) -> subsets p) ∧
(∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets p
- CLOSED_CDI_COMPL
-
|- ∀p s. closed_cdi p ∧ s ∈ subsets p ⇒ space p DIFF s ∈ subsets p
- CLOSED_CDI_DUNION
-
|- ∀p s t.
∅ ∈ subsets p ∧ closed_cdi p ∧ s ∈ subsets p ∧ t ∈ subsets p ∧
DISJOINT s t ⇒
s ∪ t ∈ subsets p
- SMALLEST_CLOSED_CDI
-
|- ∀a.
algebra a ⇒
subsets a ⊆ subsets (smallest_closed_cdi a) ∧
closed_cdi (smallest_closed_cdi a) ∧
subset_class (space a) (subsets (smallest_closed_cdi a))
- SPACE_SMALLEST_CLOSED_CDI
-
|- ∀a. space (smallest_closed_cdi a) = space a
- SPACE
-
|- ∀a. (space a,subsets a) = a
- ALGEBRA_ALT_INTER
-
|- ∀a.
algebra a ⇔
subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
(∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
∀s t. s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∩ t ∈ subsets a
- ALGEBRA_EMPTY
-
|- ∀a. algebra a ⇒ ∅ ∈ subsets a
- ALGEBRA_SPACE
-
|- ∀a. algebra a ⇒ space a ∈ subsets a
- ALGEBRA_COMPL
-
|- ∀a s. algebra a ∧ s ∈ subsets a ⇒ space a DIFF s ∈ subsets a
- ALGEBRA_UNION
-
|- ∀a s t. algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∪ t ∈ subsets a
- ALGEBRA_INTER
-
|- ∀a s t. algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∩ t ∈ subsets a
- ALGEBRA_DIFF
-
|- ∀a s t. algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒ s DIFF t ∈ subsets a
- ALGEBRA_FINITE_UNION
-
|- ∀a c. algebra a ∧ FINITE c ∧ c ⊆ subsets a ⇒ BIGUNION c ∈ subsets a
- ALGEBRA_INTER_SPACE
-
|- ∀a s. algebra a ∧ s ∈ subsets a ⇒ (space a ∩ s = s) ∧ (s ∩ space a = s)
- LAMBDA_SYSTEM_EMPTY
-
|- ∀g0 lam.
algebra g0 ∧ positive (space g0,subsets g0,lam) ⇒
∅ ∈ lambda_system g0 lam
- LAMBDA_SYSTEM_COMPL
-
|- ∀g0 lam l.
algebra g0 ∧ positive (space g0,subsets g0,lam) ∧
l ∈ lambda_system g0 lam ⇒
space g0 DIFF l ∈ lambda_system g0 lam
- LAMBDA_SYSTEM_INTER
-
|- ∀g0 lam l1 l2.
algebra g0 ∧ positive (space g0,subsets g0,lam) ∧
l1 ∈ lambda_system g0 lam ∧ l2 ∈ lambda_system g0 lam ⇒
l1 ∩ l2 ∈ lambda_system g0 lam
- LAMBDA_SYSTEM_ALGEBRA
-
|- ∀g0 lam.
algebra g0 ∧ positive (space g0,subsets g0,lam) ⇒
algebra (space g0,lambda_system g0 lam)
- LAMBDA_SYSTEM_STRONG_ADDITIVE
-
|- ∀g0 lam g l1 l2.
algebra g0 ∧ positive (space g0,subsets g0,lam) ∧ g ∈ subsets g0 ∧
DISJOINT l1 l2 ∧ l1 ∈ lambda_system g0 lam ∧ l2 ∈ lambda_system g0 lam ⇒
(lam ((l1 ∪ l2) ∩ g) = lam (l1 ∩ g) + lam (l2 ∩ g))
- LAMBDA_SYSTEM_ADDITIVE
-
|- ∀g0 lam l1 l2.
algebra g0 ∧ positive (space g0,subsets g0,lam) ⇒
additive (space g0,lambda_system g0 lam,lam)
- COUNTABLY_SUBADDITIVE_SUBADDITIVE
-
|- ∀m.
algebra (m_space m,measurable_sets m) ∧ positive m ∧
countably_subadditive m ⇒
subadditive m
- SIGMA_ALGEBRA_ALT
-
|- ∀a.
sigma_algebra a ⇔
algebra a ∧
∀f. f ∈ (𝕌(:num) -> subsets a) ⇒ BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a
- SIGMA_ALGEBRA_ALT_MONO
-
|- ∀a.
sigma_algebra a ⇔
algebra a ∧
∀f.
f ∈ (𝕌(:num) -> subsets a) ∧ (f 0 = ∅) ∧ (∀n. f n ⊆ f (SUC n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a
- SIGMA_ALGEBRA_ALT_DISJOINT
-
|- ∀a.
sigma_algebra a ⇔
algebra a ∧
∀f.
f ∈ (𝕌(:num) -> subsets a) ∧ (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a
- SUBADDITIVE
-
|- ∀m s t u.
subadditive m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
(u = s ∪ t) ⇒
measure m u ≤ measure m s + measure m t
- ADDITIVE
-
|- ∀m s t u.
additive m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
DISJOINT s t ∧ (u = s ∪ t) ⇒
(measure m u = measure m s + measure m t)
- COUNTABLY_SUBADDITIVE
-
|- ∀m f s.
countably_subadditive m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧
summable (measure m o f) ∧ (s = BIGUNION (IMAGE f 𝕌(:num))) ∧
s ∈ measurable_sets m ⇒
measure m s ≤ suminf (measure m o f)
- ADDITIVE_SUM
-
|- ∀m f n.
algebra (m_space m,measurable_sets m) ∧ positive m ∧ additive m ∧
f ∈ (𝕌(:num) -> measurable_sets m) ∧
(∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
(sum (0,n) (measure m o f) = measure m (BIGUNION (IMAGE f (count n))))
- INCREASING_ADDITIVE_SUMMABLE
-
|- ∀m f.
algebra (m_space m,measurable_sets m) ∧ positive m ∧ increasing m ∧
additive m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧
(∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
summable (measure m o f)
- LAMBDA_SYSTEM_POSITIVE
-
|- ∀g0 lam.
positive (space g0,subsets g0,lam) ⇒
positive (space g0,lambda_system g0 lam,lam)
- LAMBDA_SYSTEM_INCREASING
-
|- ∀g0 lam.
increasing (space g0,subsets g0,lam) ⇒
increasing (space g0,lambda_system g0 lam,lam)
- LAMBDA_SYSTEM_STRONG_SUM
-
|- ∀g0 lam g f n.
algebra g0 ∧ positive (space g0,subsets g0,lam) ∧ g ∈ subsets g0 ∧
f ∈ (𝕌(:num) -> lambda_system g0 lam) ∧
(∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
(sum (0,n) (lam o (λs. s ∩ g) o f) =
lam (BIGUNION (IMAGE f (count n)) ∩ g))
- SIGMA_ALGEBRA_ALGEBRA
-
|- ∀a. sigma_algebra a ⇒ algebra a
- OUTER_MEASURE_SPACE_POSITIVE
-
|- ∀m. outer_measure_space m ⇒ positive m
- LAMBDA_SYSTEM_CARATHEODORY
-
|- ∀gsig lam.
sigma_algebra gsig ∧ outer_measure_space (space gsig,subsets gsig,lam) ⇒
∀f.
f ∈ (𝕌(:num) -> lambda_system gsig lam) ∧
(∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ lambda_system gsig lam ∧
lam o f sums lam (BIGUNION (IMAGE f 𝕌(:num)))
- CARATHEODORY_LEMMA
-
|- ∀gsig lam.
sigma_algebra gsig ∧ outer_measure_space (space gsig,subsets gsig,lam) ⇒
measure_space (space gsig,lambda_system gsig lam,lam)
- INF_MEASURE_NONEMPTY
-
|- ∀m g s.
algebra (m_space m,measurable_sets m) ∧ positive m ∧
s ∈ measurable_sets m ∧ g ⊆ s ⇒
measure m s ∈
{r |
∃f.
f ∈ (𝕌(:num) -> measurable_sets m) ∧
(∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧
g ⊆ BIGUNION (IMAGE f 𝕌(:num)) ∧ measure m o f sums r}
- INF_MEASURE_POS0
-
|- ∀m g x.
algebra (m_space m,measurable_sets m) ∧ positive m ∧
x ∈
{r |
∃f.
f ∈ (𝕌(:num) -> measurable_sets m) ∧
(∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧
g ⊆ BIGUNION (IMAGE f 𝕌(:num)) ∧ measure m o f sums r} ⇒
0 ≤ x
- INF_MEASURE_POS
-
|- ∀m g.
algebra (m_space m,measurable_sets m) ∧ positive m ∧ g ⊆ m_space m ⇒
0 ≤ inf_measure m g
- INCREASING
-
|- ∀m s t.
increasing m ∧ s ⊆ t ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
measure m s ≤ measure m t
- ADDITIVE_INCREASING
-
|- ∀m.
algebra (m_space m,measurable_sets m) ∧ positive m ∧ additive m ⇒
increasing m
- COUNTABLY_ADDITIVE_ADDITIVE
-
|- ∀m.
algebra (m_space m,measurable_sets m) ∧ positive m ∧
countably_additive m ⇒
additive m
- COUNTABLY_ADDITIVE
-
|- ∀m s f.
countably_additive m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧
(∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧ (s = BIGUNION (IMAGE f 𝕌(:num))) ∧
s ∈ measurable_sets m ⇒
measure m o f sums measure m s
- INF_MEASURE_AGREES
-
|- ∀m s.
algebra (m_space m,measurable_sets m) ∧ positive m ∧
countably_additive m ∧ s ∈ measurable_sets m ⇒
(inf_measure m s = measure m s)
- MEASURE_DOWN
-
|- ∀m0 m1.
sigma_algebra (m_space m0,measurable_sets m0) ∧
measurable_sets m0 ⊆ measurable_sets m1 ∧ (measure m0 = measure m1) ∧
measure_space m1 ⇒
measure_space m0
- SIGMA_ALGEBRA_SIGMA
-
|- ∀sp sts. subset_class sp sts ⇒ sigma_algebra (sigma sp sts)
- POW_ALGEBRA
-
|- algebra (sp,POW sp)
- POW_SIGMA_ALGEBRA
-
|- sigma_algebra (sp,POW sp)
- UNIV_SIGMA_ALGEBRA
-
|- sigma_algebra (𝕌(:α),𝕌(:α -> bool))
- INF_MEASURE_EMPTY
-
|- ∀m.
algebra (m_space m,measurable_sets m) ∧ positive m ⇒
(inf_measure m ∅ = 0)
- INF_MEASURE_POSITIVE
-
|- ∀m.
algebra (m_space m,measurable_sets m) ∧ positive m ⇒
positive (m_space m,POW (m_space m),inf_measure m)
- INF_MEASURE_INCREASING
-
|- ∀m.
algebra (m_space m,measurable_sets m) ∧ positive m ⇒
increasing (m_space m,POW (m_space m),inf_measure m)
- INF_MEASURE_LE
-
|- ∀m s x.
algebra (m_space m,measurable_sets m) ∧ positive m ∧ increasing m ∧
x ∈
{r |
∃f.
f ∈ (𝕌(:num) -> measurable_sets m) ∧ s ⊆ BIGUNION (IMAGE f 𝕌(:num)) ∧
measure m o f sums r} ⇒
inf_measure m s ≤ x
- INF_MEASURE_CLOSE
-
|- ∀m s e.
algebra (m_space m,measurable_sets m) ∧ positive m ∧ 0 < e ∧
s ⊆ m_space m ⇒
∃f l.
f ∈ (𝕌(:num) -> measurable_sets m) ∧ s ⊆ BIGUNION (IMAGE f 𝕌(:num)) ∧
(∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧ measure m o f sums l ∧
l ≤ inf_measure m s + e
- INF_MEASURE_COUNTABLY_SUBADDITIVE
-
|- ∀m.
algebra (m_space m,measurable_sets m) ∧ positive m ∧ increasing m ⇒
countably_subadditive (m_space m,POW (m_space m),inf_measure m)
- INF_MEASURE_OUTER
-
|- ∀m.
algebra (m_space m,measurable_sets m) ∧ positive m ∧ increasing m ⇒
outer_measure_space (m_space m,POW (m_space m),inf_measure m)
- SIGMA_SUBSET
-
|- ∀a b.
sigma_algebra b ∧ a ⊆ subsets b ⇒ subsets (sigma (space b) a) ⊆ subsets b
- ALGEBRA_SUBSET_LAMBDA_SYSTEM
-
|- ∀m.
algebra (m_space m,measurable_sets m) ∧ positive m ∧ increasing m ∧
additive m ⇒
measurable_sets m ⊆
lambda_system (m_space m,POW (m_space m)) (inf_measure m)
- CARATHEODORY
-
|- ∀m0.
algebra (m_space m0,measurable_sets m0) ∧ positive m0 ∧
countably_additive m0 ⇒
∃m.
(∀s. s ∈ measurable_sets m0 ⇒ (measure m s = measure m0 s)) ∧
((m_space m,measurable_sets m) =
sigma (m_space m0) (measurable_sets m0)) ∧ measure_space m
- SIGMA_SUBSET_SUBSETS
-
|- ∀sp a. a ⊆ subsets (sigma sp a)
- IN_SIGMA
-
|- ∀sp a x. x ∈ a ⇒ x ∈ subsets (sigma sp a)
- SIGMA_ALGEBRA
-
|- ∀p.
sigma_algebra p ⇔
subset_class (space p) (subsets p) ∧ ∅ ∈ subsets p ∧
(∀s. s ∈ subsets p ⇒ space p DIFF s ∈ subsets p) ∧
∀c. countable c ∧ c ⊆ subsets p ⇒ BIGUNION c ∈ subsets p
- SIGMA_ALGEBRA_COUNTABLE_UNION
-
|- ∀a c.
sigma_algebra a ∧ countable c ∧ c ⊆ subsets a ⇒ BIGUNION c ∈ subsets a
- SIGMA_ALGEBRA_ENUM
-
|- ∀a f.
sigma_algebra a ∧ f ∈ (𝕌(:num) -> subsets a) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a
- MEASURE_COMPL
-
|- ∀m s.
measure_space m ∧ s ∈ measurable_sets m ⇒
(measure m (m_space m DIFF s) = measure m (m_space m) − measure m s)
- SIGMA_PROPERTY
-
|- ∀sp p a.
subset_class sp p ∧ ∅ ∈ p ∧ a ⊆ p ∧
(∀s. s ∈ p ∩ subsets (sigma sp a) ⇒ sp DIFF s ∈ p) ∧
(∀c. countable c ∧ c ⊆ p ∩ subsets (sigma sp a) ⇒ BIGUNION c ∈ p) ⇒
subsets (sigma sp a) ⊆ p
- MEASURE_EMPTY
-
|- ∀m. measure_space m ⇒ (measure m ∅ = 0)
- SIGMA_SUBSET_MEASURABLE_SETS
-
|- ∀a m.
measure_space m ∧ a ⊆ measurable_sets m ⇒
subsets (sigma (m_space m) a) ⊆ measurable_sets m
- SIGMA_ALGEBRA_FN
-
|- ∀a.
sigma_algebra a ⇔
subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
(∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
∀f. f ∈ (𝕌(:num) -> subsets a) ⇒ BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a
- SIGMA_ALGEBRA_FN_DISJOINT
-
|- ∀a.
sigma_algebra a ⇔
subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
(∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
(∀s t. s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∪ t ∈ subsets a) ∧
∀f.
f ∈ (𝕌(:num) -> subsets a) ∧ (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a
- SIGMA_PROPERTY_ALT
-
|- ∀sp p a.
subset_class sp p ∧ ∅ ∈ p ∧ a ⊆ p ∧
(∀s. s ∈ p ∩ subsets (sigma sp a) ⇒ sp DIFF s ∈ p) ∧
(∀f.
f ∈ (𝕌(:num) -> p ∩ subsets (sigma sp a)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ⇒
subsets (sigma sp a) ⊆ p
- SIGMA_PROPERTY_DISJOINT_WEAK
-
|- ∀sp p a.
algebra (sp,a) ∧ a ⊆ p ∧ subset_class sp p ∧
(∀s. s ∈ p ⇒ sp DIFF s ∈ p) ∧
(∀f.
f ∈ (𝕌(:num) -> p) ∧ (f 0 = ∅) ∧ (∀n. f n ⊆ f (SUC n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ∧
(∀f.
f ∈ (𝕌(:num) -> p) ∧ (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ⇒
subsets (sigma sp a) ⊆ p
- SIGMA_PROPERTY_DISJOINT
-
|- ∀sp p a.
algebra (sp,a) ∧ a ⊆ p ∧
(∀s. s ∈ p ∩ subsets (sigma sp a) ⇒ sp DIFF s ∈ p) ∧
(∀f.
f ∈ (𝕌(:num) -> p ∩ subsets (sigma sp a)) ∧ (f 0 = ∅) ∧
(∀n. f n ⊆ f (SUC n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ∧
(∀f.
f ∈ (𝕌(:num) -> p ∩ subsets (sigma sp a)) ∧
(∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ⇒
subsets (sigma sp a) ⊆ p
- MEASURE_COUNTABLY_ADDITIVE
-
|- ∀m s f.
measure_space m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧
(∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧ (s = BIGUNION (IMAGE f 𝕌(:num))) ⇒
measure m o f sums measure m s
- MEASURE_SPACE_ADDITIVE
-
|- ∀m. measure_space m ⇒ additive m
- MEASURE_ADDITIVE
-
|- ∀m s t u.
measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
DISJOINT s t ∧ (u = s ∪ t) ⇒
(measure m u = measure m s + measure m t)
- MEASURE_COUNTABLE_INCREASING
-
|- ∀m s f.
measure_space m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧ (f 0 = ∅) ∧
(∀n. f n ⊆ f (SUC n)) ∧ (s = BIGUNION (IMAGE f 𝕌(:num))) ⇒
measure m o f --> measure m s
- MEASURE_SPACE_REDUCE
-
|- ∀m. (m_space m,measurable_sets m,measure m) = m
- SPACE_SIGMA
-
|- ∀sp a. space (sigma sp a) = sp
- MONOTONE_CONVERGENCE
-
|- ∀m s f.
measure_space m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧
(∀n. f n ⊆ f (SUC n)) ∧ (s = BIGUNION (IMAGE f 𝕌(:num))) ⇒
measure m o f --> measure m s
- SIGMA_REDUCE
-
|- ∀sp a. (sp,subsets (sigma sp a)) = sigma sp a
- MEASURABLE_SETS_SUBSET_SPACE
-
|- ∀m s. measure_space m ∧ s ∈ measurable_sets m ⇒ s ⊆ m_space m
- MEASURABLE_DIFF_PROPERTY
-
|- ∀a b f.
sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a -> space b) ∧
(∀s. s ∈ subsets b ⇒ PREIMAGE f s ∈ subsets a) ⇒
∀s.
s ∈ subsets b ⇒
(PREIMAGE f (space b DIFF s) = space a DIFF PREIMAGE f s)
- MEASURABLE_BIGUNION_PROPERTY
-
|- ∀a b f.
sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a -> space b) ∧
(∀s. s ∈ subsets b ⇒ PREIMAGE f s ∈ subsets a) ⇒
∀c.
c ⊆ subsets b ⇒
(PREIMAGE f (BIGUNION c) = BIGUNION (IMAGE (PREIMAGE f) c))
- MEASUBABLE_BIGUNION_LEMMA
-
|- ∀a b f.
sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a -> space b) ∧
(∀s. s ∈ subsets b ⇒ PREIMAGE f s ∈ subsets a) ⇒
∀c.
countable c ∧ c ⊆ IMAGE (PREIMAGE f) (subsets b) ⇒
BIGUNION c ∈ IMAGE (PREIMAGE f) (subsets b)
- MEASURABLE_SIGMA_PREIMAGES
-
|- ∀a b f.
sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a -> space b) ∧
(∀s. s ∈ subsets b ⇒ PREIMAGE f s ∈ subsets a) ⇒
sigma_algebra (space a,IMAGE (PREIMAGE f) (subsets b))
- IN_MEASURABLE
-
|- ∀a b f.
f ∈ measurable a b ⇔
sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a -> space b) ∧
∀s. s ∈ subsets b ⇒ PREIMAGE f s ∩ space a ∈ subsets a
- MEASURABLE_SIGMA
-
|- ∀f a b sp.
sigma_algebra a ∧ subset_class sp b ∧ f ∈ (space a -> sp) ∧
(∀s. s ∈ b ⇒ PREIMAGE f s ∩ space a ∈ subsets a) ⇒
f ∈ measurable a (sigma sp b)
- MEASURABLE_SUBSET
-
|- ∀a b. measurable a b ⊆ measurable a (sigma (space b) (subsets b))
- MEASURABLE_LIFT
-
|- ∀f a b. f ∈ measurable a b ⇒ f ∈ measurable a (sigma (space b) (subsets b))
- IN_MEASURE_PRESERVING
-
|- ∀m1 m2 f.
f ∈ measure_preserving m1 m2 ⇔
f ∈
measurable (m_space m1,measurable_sets m1)
(m_space m2,measurable_sets m2) ∧ measure_space m1 ∧ measure_space m2 ∧
∀s.
s ∈ measurable_sets m2 ⇒
(measure m1 (PREIMAGE f s ∩ m_space m1) = measure m2 s)
- MEASURE_PRESERVING_LIFT
-
|- ∀m1 m2 a f.
measure_space m1 ∧ measure_space m2 ∧
(measurable_sets m2 = subsets (sigma (m_space m2) a)) ∧
f ∈ measure_preserving m1 (m_space m2,a,measure m2) ⇒
f ∈ measure_preserving m1 m2
- MEASURE_PRESERVING_SUBSET
-
|- ∀m1 m2 a.
measure_space m1 ∧ measure_space m2 ∧
(measurable_sets m2 = subsets (sigma (m_space m2) a)) ⇒
measure_preserving m1 (m_space m2,a,measure m2) ⊆
measure_preserving m1 m2
- MEASURABLE_I
-
|- ∀a. sigma_algebra a ⇒ I ∈ measurable a a
- MEASURABLE_COMP
-
|- ∀f g a b c.
f ∈ measurable a b ∧ g ∈ measurable b c ⇒ g o f ∈ measurable a c
- MEASURABLE_COMP_STRONG
-
|- ∀f g a b c.
f ∈ measurable a b ∧ sigma_algebra c ∧ g ∈ (space b -> space c) ∧
(∀x. x ∈ subsets c ⇒ PREIMAGE g x ∩ IMAGE f (space a) ∈ subsets b) ⇒
g o f ∈ measurable a c
- MEASURABLE_COMP_STRONGER
-
|- ∀f g a b c t.
f ∈ measurable a b ∧ sigma_algebra c ∧ g ∈ (space b -> space c) ∧
IMAGE f (space a) ⊆ t ∧
(∀s. s ∈ subsets c ⇒ PREIMAGE g s ∩ t ∈ subsets b) ⇒
g o f ∈ measurable a c
- MEASURABLE_UP_LIFT
-
|- ∀sp a b c f.
f ∈ measurable (sp,a) c ∧ sigma_algebra (sp,b) ∧ a ⊆ b ⇒
f ∈ measurable (sp,b) c
- MEASURABLE_UP_SUBSET
-
|- ∀sp a b c.
a ⊆ b ∧ sigma_algebra (sp,b) ⇒ measurable (sp,a) c ⊆ measurable (sp,b) c
- MEASURABLE_UP_SIGMA
-
|- ∀a b. measurable a b ⊆ measurable (sigma (space a) (subsets a)) b
- MEASURE_PRESERVING_UP_LIFT
-
|- ∀m1 m2 f.
measure_space m1 ∧ f ∈ measure_preserving (m_space m1,a,measure m1) m2 ∧
sigma_algebra (m_space m1,measurable_sets m1) ∧ a ⊆ measurable_sets m1 ⇒
f ∈ measure_preserving m1 m2
- MEASURE_PRESERVING_UP_SUBSET
-
|- ∀m1 m2.
measure_space m1 ∧ a ⊆ measurable_sets m1 ∧
sigma_algebra (m_space m1,measurable_sets m1) ⇒
measure_preserving (m_space m1,a,measure m1) m2 ⊆
measure_preserving m1 m2
- MEASURE_PRESERVING_UP_SIGMA
-
|- ∀m1 m2 a.
measure_space m1 ∧
(measurable_sets m1 = subsets (sigma (m_space m1) a)) ⇒
measure_preserving (m_space m1,a,measure m1) m2 ⊆
measure_preserving m1 m2
- MEASURABLE_PROD_SIGMA
-
|- ∀a a1 a2 f.
sigma_algebra a ∧ FST o f ∈ measurable a a1 ∧ SND o f ∈ measurable a a2 ⇒
f ∈
measurable a
(sigma (space a1 × space a2) (prod_sets (subsets a1) (subsets a2)))
- MEASURABLE_RANGE_REDUCE
-
|- ∀m f s.
measure_space m ∧
f ∈ measurable (m_space m,measurable_sets m) (s,POW s) ∧ s ≠ ∅ ⇒
f ∈
measurable (m_space m,measurable_sets m)
(s ∩ IMAGE f (m_space m),POW (s ∩ IMAGE f (m_space m)))
- MEASURABLE_POW_TO_POW
-
|- ∀m f.
measure_space m ∧ (measurable_sets m = POW (m_space m)) ⇒
f ∈ measurable (m_space m,measurable_sets m) (𝕌(:β),POW 𝕌(:β))
- MEASURABLE_POW_TO_POW_IMAGE
-
|- ∀m f.
measure_space m ∧ (measurable_sets m = POW (m_space m)) ⇒
f ∈
measurable (m_space m,measurable_sets m)
(IMAGE f (m_space m),POW (IMAGE f (m_space m)))
- MEASURE_SPACE_SUBSET
-
|- ∀s s' m. s' ⊆ s ∧ measure_space (s,POW s,m) ⇒ measure_space (s',POW s',m)
- STRONG_MEASURE_SPACE_SUBSET
-
|- ∀s s'.
s' ⊆ m_space s ∧ measure_space s ∧ POW s' ⊆ measurable_sets s ⇒
measure_space (s',POW s',measure s)
- MEASURE_REAL_SUM_IMAGE
-
|- ∀m s.
measure_space m ∧ s ∈ measurable_sets m ∧
(∀x. x ∈ s ⇒ {x} ∈ measurable_sets m) ∧ FINITE s ⇒
(measure m s = SIGMA (λx. measure m {x}) s)
- SIGMA_POW
-
|- ∀s. sigma s (POW s) = (s,POW s)
- finite_additivity_sufficient_for_finite_spaces
-
|- ∀s m.
sigma_algebra s ∧ FINITE (space s) ∧ positive (space s,subsets s,m) ∧
additive (space s,subsets s,m) ⇒
measure_space (space s,subsets s,m)
- finite_additivity_sufficient_for_finite_spaces2
-
|- ∀m.
sigma_algebra (m_space m,measurable_sets m) ∧ FINITE (m_space m) ∧
positive m ∧ additive m ⇒
measure_space m
- IMAGE_SING
-
|- ∀f x. IMAGE f {x} = {f x}
- SUBSET_BIGINTER
-
|- ∀X P. X ⊆ BIGINTER P ⇔ ∀Y. Y ∈ P ⇒ X ⊆ Y
- MEASURE_SPACE_INCREASING
-
|- ∀m. measure_space m ⇒ increasing m
- MEASURE_SPACE_POSITIVE
-
|- ∀m. measure_space m ⇒ positive m
- MEASURE_SPACE_INTER
-
|- ∀m s t.
measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
s ∩ t ∈ measurable_sets m
- MEASURE_SPACE_UNION
-
|- ∀m s t.
measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
s ∪ t ∈ measurable_sets m
- MEASURE_SPACE_DIFF
-
|- ∀m s t.
measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
s DIFF t ∈ measurable_sets m
- MEASURE_COMPL_SUBSET
-
|- ∀m s.
measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧ t ⊆ s ⇒
(measure m (s DIFF t) = measure m s − measure m t)
- MEASURE_SPACE_BIGUNION
-
|- ∀m s.
measure_space m ∧ (∀n. s n ∈ measurable_sets m) ⇒
BIGUNION (IMAGE s 𝕌(:num)) ∈ measurable_sets m
- MEASURE_SPACE_IN_MSPACE
-
|- ∀m A. measure_space m ∧ A ∈ measurable_sets m ⇒ ∀x. x ∈ A ⇒ x ∈ m_space m
- MEASURE_SPACE_SUBSET_MSPACE
-
|- ∀A m. measure_space m ∧ A ∈ measurable_sets m ⇒ A ⊆ m_space m
- MEASURE_SPACE_EMPTY_MEASURABLE
-
|- ∀m. measure_space m ⇒ ∅ ∈ measurable_sets m
- MEASURE_SPACE_MSPACE_MEASURABLE
-
|- ∀m. measure_space m ⇒ m_space m ∈ measurable_sets m
- SIGMA_ALGEBRA_FN_BIGINTER
-
|- ∀a.
sigma_algebra a ⇒
subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
(∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
∀f. f ∈ (𝕌(:num) -> subsets a) ⇒ BIGINTER (IMAGE f 𝕌(:num)) ∈ subsets a
- MEASURE_SPACE_BIGINTER
-
|- ∀m s.
measure_space m ∧ (∀n. s n ∈ measurable_sets m) ⇒
BIGINTER (IMAGE s 𝕌(:num)) ∈ measurable_sets m
- MONOTONE_CONVERGENCE2
-
|- ∀m f.
measure_space m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧
(∀n. f n ⊆ f (SUC n)) ⇒
measure m o f --> measure m (BIGUNION (IMAGE f 𝕌(:num)))
- MONOTONE_CONVERGENCE_BIGINTER
-
|- ∀m s f.
measure_space m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧
(∀n. f (SUC n) ⊆ f n) ∧ (s = BIGINTER (IMAGE f 𝕌(:num))) ⇒
measure m o f --> measure m s
- MONOTONE_CONVERGENCE_BIGINTER2
-
|- ∀m f.
measure_space m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧
(∀n. f (SUC n) ⊆ f n) ⇒
measure m o f --> measure m (BIGINTER (IMAGE f 𝕌(:num)))
- MEASURE_SPACE_RESTRICTED
-
|- ∀m s.
measure_space m ∧ s ∈ measurable_sets m ⇒
measure_space (s,IMAGE (λt. s ∩ t) (measurable_sets m),measure m)
- MEASURE_SPACE_CMUL
-
|- ∀m c.
measure_space m ∧ 0 ≤ c ⇒
measure_space (m_space m,measurable_sets m,(λa. c * measure m a))
- BIGUNION_IMAGE_Q
-
|- ∀a f.
sigma_algebra a ∧ f ∈ (Q_set -> subsets a) ⇒
BIGUNION (IMAGE f Q_set) ∈ subsets a
- SIGMA_ALGEBRA_BOREL
-
|- sigma_algebra Borel
- MEASURABLE_BOREL
-
|- ∀f a.
f ∈ measurable a Borel ⇔
sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
∀c. PREIMAGE f {x | x < c} ∩ space a ∈ subsets a
- IN_MEASURABLE_BOREL
-
|- ∀f a.
f ∈ measurable a Borel ⇔
sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
∀c. {x | f x < c} ∩ space a ∈ subsets a
- IN_MEASURABLE_BOREL_NEGINF
-
|- ∀f a. f ∈ measurable a Borel ⇒ {x | f x = NegInf} ∩ space a ∈ subsets a
- IN_MEASURABLE_BOREL_ALT1
-
|- ∀f a.
f ∈ measurable a Borel ⇔
sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
∀c. {x | c ≤ f x} ∩ space a ∈ subsets a
- IN_MEASURABLE_BOREL_ALT2
-
|- ∀f a.
f ∈ measurable a Borel ⇔
sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
∀c. {x | f x ≤ c} ∩ space a ∈ subsets a
- IN_MEASURABLE_BOREL_ALT3
-
|- ∀f a.
f ∈ measurable a Borel ⇔
sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
∀c. {x | c < f x} ∩ space a ∈ subsets a
- IN_MEASURABLE_BOREL_ALT4
-
|- ∀f a.
f ∈ measurable a Borel ⇔
sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
∀c d. {x | c ≤ f x ∧ f x < d} ∩ space a ∈ subsets a
- IN_MEASURABLE_BOREL_ALT5
-
|- ∀f a.
f ∈ measurable a Borel ⇔
sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
∀c d. {x | c < f x ∧ f x ≤ d} ∩ space a ∈ subsets a
- IN_MEASURABLE_BOREL_ALT6
-
|- ∀f a.
f ∈ measurable a Borel ⇔
sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
∀c d. {x | c ≤ f x ∧ f x ≤ d} ∩ space a ∈ subsets a
- IN_MEASURABLE_BOREL_ALT7
-
|- ∀f a.
f ∈ measurable a Borel ⇒
sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
∀c d. {x | c < f x ∧ f x < d} ∩ space a ∈ subsets a
- IN_MEASURABLE_BOREL_ALT8
-
|- ∀f a.
f ∈ measurable a Borel ⇒
sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
∀c. {x | f x = c} ∩ space a ∈ subsets a
- IN_MEASURABLE_BOREL_ALT9
-
|- ∀f a.
f ∈ measurable a Borel ⇒
sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
∀c. {x | f x ≠ c} ∩ space a ∈ subsets a
- IN_MEASURABLE_BOREL_ALL
-
|- ∀f a.
f ∈ measurable a Borel ⇒
(∀c. {x | f x < c} ∩ space a ∈ subsets a) ∧
(∀c. {x | c ≤ f x} ∩ space a ∈ subsets a) ∧
(∀c. {x | f x ≤ c} ∩ space a ∈ subsets a) ∧
(∀c. {x | c < f x} ∩ space a ∈ subsets a) ∧
(∀c d. {x | c < f x ∧ f x < d} ∩ space a ∈ subsets a) ∧
(∀c d. {x | c ≤ f x ∧ f x < d} ∩ space a ∈ subsets a) ∧
(∀c d. {x | c < f x ∧ f x ≤ d} ∩ space a ∈ subsets a) ∧
(∀c d. {x | c ≤ f x ∧ f x ≤ d} ∩ space a ∈ subsets a) ∧
(∀c. {x | f x ≠ c} ∩ space a ∈ subsets a) ∧
∀c. {x | f x = c} ∩ space a ∈ subsets a
- IN_MEASURABLE_BOREL_ALL_MEASURE
-
|- ∀f m.
f ∈ measurable (m_space m,measurable_sets m) Borel ⇒
(∀c. {x | f x < c} ∩ m_space m ∈ measurable_sets m) ∧
(∀c. {x | c ≤ f x} ∩ m_space m ∈ measurable_sets m) ∧
(∀c. {x | f x ≤ c} ∩ m_space m ∈ measurable_sets m) ∧
(∀c. {x | c < f x} ∩ m_space m ∈ measurable_sets m) ∧
(∀c d. {x | c < f x ∧ f x < d} ∩ m_space m ∈ measurable_sets m) ∧
(∀c d. {x | c ≤ f x ∧ f x < d} ∩ m_space m ∈ measurable_sets m) ∧
(∀c d. {x | c < f x ∧ f x ≤ d} ∩ m_space m ∈ measurable_sets m) ∧
(∀c d. {x | c ≤ f x ∧ f x ≤ d} ∩ m_space m ∈ measurable_sets m) ∧
(∀c. {x | f x = c} ∩ m_space m ∈ measurable_sets m) ∧
∀c. {x | f x ≠ c} ∩ m_space m ∈ measurable_sets m
- IN_MEASURABLE_BOREL_LT
-
|- ∀f g a.
f ∈ measurable a Borel ∧ g ∈ measurable a Borel ⇒
{x | f x < g x} ∩ space a ∈ subsets a
- IN_MEASURABLE_BOREL_LE
-
|- ∀f g a.
f ∈ measurable a Borel ∧ g ∈ measurable a Borel ⇒
{x | f x ≤ g x} ∩ space a ∈ subsets a
- SPACE_BOREL
-
|- space Borel = 𝕌(:extreal)
- BOREL_MEASURABLE_SETS1
-
|- ∀c. {x | x < c} ∈ subsets Borel
- BOREL_MEASURABLE_SETS2
-
|- ∀c. {x | c ≤ x} ∈ subsets Borel
- BOREL_MEASURABLE_SETS3
-
|- ∀c. {x | x ≤ c} ∈ subsets Borel
- BOREL_MEASURABLE_SETS4
-
|- ∀c. {x | c < x} ∈ subsets Borel
- BOREL_MEASURABLE_SETS5
-
|- ∀c d. {x | c ≤ x ∧ x < d} ∈ subsets Borel
- BOREL_MEASURABLE_SETS6
-
|- ∀c d. {x | c < x ∧ x ≤ d} ∈ subsets Borel
- BOREL_MEASURABLE_SETS7
-
|- ∀c d. {x | c ≤ x ∧ x ≤ d} ∈ subsets Borel
- BOREL_MEASURABLE_SETS8
-
|- ∀c d. {x | c < x ∧ x < d} ∈ subsets Borel
- BOREL_MEASURABLE_SETS9
-
|- ∀c. {c} ∈ subsets Borel
- BOREL_MEASURABLE_SETS10
-
|- ∀c. {x | x ≠ c} ∈ subsets Borel
- BOREL_MEASURABLE_SETS
-
|- (∀c. {x | x < c} ∈ subsets Borel) ∧ (∀c. {x | c ≤ x} ∈ subsets Borel) ∧
(∀c. {x | c < x} ∈ subsets Borel) ∧ (∀c. {x | x ≤ c} ∈ subsets Borel) ∧
(∀c d. {x | c < x ∧ x < d} ∈ subsets Borel) ∧
(∀c d. {x | c ≤ x ∧ x < d} ∈ subsets Borel) ∧
(∀c d. {x | c < x ∧ x ≤ d} ∈ subsets Borel) ∧
(∀c d. {x | c ≤ x ∧ x ≤ d} ∈ subsets Borel) ∧ (∀c. {c} ∈ subsets Borel) ∧
∀c. {x | x ≠ c} ∈ subsets Borel
- IN_MEASURABLE_BOREL_CONST
-
|- ∀a k f.
sigma_algebra a ∧ (∀x. x ∈ space a ⇒ (f x = k)) ⇒ f ∈ measurable a Borel
- IN_MEASURABLE_BOREL_INDICATOR
-
|- ∀a A f.
sigma_algebra a ∧ A ∈ subsets a ∧
(∀x. x ∈ space a ⇒ (f x = indicator_fn A x)) ⇒
f ∈ measurable a Borel
- IN_MEASURABLE_BOREL_CMUL
-
|- ∀a f g z.
sigma_algebra a ∧ f ∈ measurable a Borel ∧
(∀x. x ∈ space a ⇒ (g x = Normal z * f x)) ⇒
g ∈ measurable a Borel
- IN_MEASURABLE_BOREL_ABS
-
|- ∀a f g.
sigma_algebra a ∧ f ∈ measurable a Borel ∧
(∀x. x ∈ space a ⇒ (g x = abs (f x))) ⇒
g ∈ measurable a Borel
- IN_MEASURABLE_BOREL_SQR
-
|- ∀a f g.
sigma_algebra a ∧ f ∈ measurable a Borel ∧
(∀x. x ∈ space a ⇒ (g x = f x pow 2)) ⇒
g ∈ measurable a Borel
- IN_MEASURABLE_BOREL_ADD
-
|- ∀a f g h.
sigma_algebra a ∧ f ∈ measurable a Borel ∧ g ∈ measurable a Borel ∧
(∀x. x ∈ space a ⇒ (h x = f x + g x)) ⇒
h ∈ measurable a Borel
- IN_MEASURABLE_BOREL_SUB
-
|- ∀a f g h.
sigma_algebra a ∧ f ∈ measurable a Borel ∧ g ∈ measurable a Borel ∧
(∀x. x ∈ space a ⇒ (h x = f x − g x)) ⇒
h ∈ measurable a Borel
- IN_MEASURABLE_BOREL_MUL
-
|- ∀a f g h.
sigma_algebra a ∧ f ∈ measurable a Borel ∧
(∀x.
x ∈ space a ⇒
f x ≠ NegInf ∧ f x ≠ PosInf ∧ g x ≠ NegInf ∧ g x ≠ PosInf) ∧
g ∈ measurable a Borel ∧ (∀x. x ∈ space a ⇒ (h x = f x * g x)) ⇒
h ∈ measurable a Borel
- IN_MEASURABLE_BOREL_SUM
-
|- ∀a f g s.
FINITE s ∧ sigma_algebra a ∧ (∀i. i ∈ s ⇒ f i ∈ measurable a Borel) ∧
(∀x. x ∈ space a ⇒ (g x = SIGMA (λi. f i x) s)) ⇒
g ∈ measurable a Borel
- IN_MEASURABLE_BOREL_CMUL_INDICATOR
-
|- ∀a z s.
sigma_algebra a ∧ s ∈ subsets a ⇒
(λx. Normal z * indicator_fn s x) ∈ measurable a Borel
- IN_MEASURABLE_BOREL_MUL_INDICATOR
-
|- ∀a f s.
sigma_algebra a ∧ f ∈ measurable a Borel ∧ s ∈ subsets a ⇒
(λx. f x * indicator_fn s x) ∈ measurable a Borel
- IN_MEASURABLE_BOREL_MUL_INDICATOR_EQ
-
|- ∀a f.
sigma_algebra a ⇒
(f ∈ measurable a Borel ⇔
(λx. f x * indicator_fn (space a) x) ∈ measurable a Borel)
- IN_MEASURABLE_BOREL_POS_SIMPLE_FN
-
|- ∀m f.
measure_space m ∧ (∃s a x. pos_simple_fn m f s a x) ⇒
f ∈ measurable (m_space m,measurable_sets m) Borel
- IN_MEASURABLE_BOREL_POW
-
|- ∀n a f.
sigma_algebra a ∧ f ∈ measurable a Borel ∧
(∀x. x ∈ space a ⇒ f x ≠ NegInf ∧ f x ≠ PosInf) ⇒
(λx. f x pow n) ∈ measurable a Borel
- IN_MEASURABLE_BOREL_MAX
-
|- ∀a f g.
sigma_algebra a ∧ f ∈ measurable a Borel ∧ g ∈ measurable a Borel ⇒
(λx. max (f x) (g x)) ∈ measurable a Borel
- IN_MEASURABLE_BOREL_MONO_SUP
-
|- ∀fn f a.
sigma_algebra a ∧ (∀n. fn n ∈ measurable a Borel) ∧
(∀n x. x ∈ space a ⇒ fn n x ≤ fn (SUC n) x) ∧
(∀x. x ∈ space a ⇒ (f x = sup (IMAGE (λn. fn n x) 𝕌(:num)))) ⇒
f ∈ measurable a Borel
- FN_PLUS_POS
-
|- ∀g x. 0 ≤ fn_plus g x
- FN_MINUS_POS
-
|- ∀g x. 0 ≤ fn_minus g x
- FN_PLUS_POS_ID
-
|- (∀x. 0 ≤ g x) ⇒ (fn_plus g = g)
- FN_MINUS_POS_ZERO
-
|- (∀x. 0 ≤ g x) ⇒ (fn_minus g = (λx. 0))
- FN_PLUS_CMUL
-
|- ∀f c.
(0 ≤ c ⇒ (fn_plus (λx. Normal c * f x) = (λx. Normal c * fn_plus f x))) ∧
(c ≤ 0 ⇒ (fn_plus (λx. Normal c * f x) = (λx. -Normal c * fn_minus f x)))
- FN_MINUS_CMUL
-
|- ∀f c.
(0 ≤ c ⇒
(fn_minus (λx. Normal c * f x) = (λx. Normal c * fn_minus f x))) ∧
(c ≤ 0 ⇒ (fn_minus (λx. Normal c * f x) = (λx. -Normal c * fn_plus f x)))
- FN_PLUS_ADD_LE
-
|- ∀f g x. fn_plus (λx. f x + g x) x ≤ fn_plus f x + fn_plus g x
- FN_MINUS_ADD_LE
-
|- ∀f g x. fn_minus (λx. f x + g x) x ≤ fn_minus f x + fn_minus g x
- IN_MEASURABLE_BOREL_FN_PLUS
-
|- ∀a f. f ∈ measurable a Borel ⇒ fn_plus f ∈ measurable a Borel
- IN_MEASURABLE_BOREL_FN_MINUS
-
|- ∀a f. f ∈ measurable a Borel ⇒ fn_minus f ∈ measurable a Borel
- IN_MEASURABLE_BOREL_PLUS_MINUS
-
|- ∀a f.
f ∈ measurable a Borel ⇔
fn_plus f ∈ measurable a Borel ∧ fn_minus f ∈ measurable a Borel
- INDICATOR_FN_MUL_INTER
-
|- ∀A B.
(λt. indicator_fn A t * indicator_fn B t) = (λt. indicator_fn (A ∩ B) t)
- indicator_fn_split
-
|- ∀r s b.
FINITE r ∧ (BIGUNION (IMAGE b r) = s) ∧
(∀i j. i ∈ r ∧ j ∈ r ∧ i ≠ j ⇒ DISJOINT (b i) (b j)) ⇒
∀a.
a ⊆ s ⇒ (indicator_fn a = (λx. SIGMA (λi. indicator_fn (a ∩ b i) x) r))
- indicator_fn_suminf
-
|- ∀a x.
(∀m n. m ≠ n ⇒ DISJOINT (a m) (a n)) ⇒
(suminf (λi. indicator_fn (a i) x) =
indicator_fn (BIGUNION (IMAGE a 𝕌(:num))) x)
- measure_split
-
|- ∀r b m.
measure_space m ∧ FINITE r ∧ (BIGUNION (IMAGE b r) = m_space m) ∧
(∀i j. i ∈ r ∧ j ∈ r ∧ i ≠ j ⇒ DISJOINT (b i) (b j)) ∧
(∀i. i ∈ r ⇒ b i ∈ measurable_sets m) ⇒
∀a.
a ∈ measurable_sets m ⇒
(measure m a = SIGMA (λi. measure m (a ∩ b i)) r)