ovollb

Description: The outer volume is a lower bound on the sum of all interval coverings of A . (Contributed by Mario Carneiro, 15-Jun-2014)

		Ref	Expression
	Hypothesis	ovollb.1	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
	Assertion	ovollb	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ((.) \circ F)) \to {vol}^{} (A) \leq sup (ran S ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		ovollb.1	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
2		simpr	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ((.) \circ F)) \to A \subseteq ⋃ ran ((.) \circ F)$
3		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
4		simpl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ((.) \circ F)) \to F : ℕ ⟶ \leq \cap ℝ^{2}$
5		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
6		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
7	5 6	sstri	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
8		fss	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}) \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
9	4 7 8	sylancl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ((.) \circ F)) \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
10		fco	$⊢ ((.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \land F : ℕ ⟶ ℝ^{} \times ℝ^{}) \to ((.) \circ F) : ℕ ⟶ 𝒫 ℝ$
11	3 9 10	sylancr	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ((.) \circ F)) \to ((.) \circ F) : ℕ ⟶ 𝒫 ℝ$
12	11	frnd	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ((.) \circ F)) \to ran ((.) \circ F) \subseteq 𝒫 ℝ$
13		sspwuni	$⊢ ran ((.) \circ F) \subseteq 𝒫 ℝ \leftrightarrow ⋃ ran ((.) \circ F) \subseteq ℝ$
14	12 13	sylib	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ((.) \circ F)) \to ⋃ ran ((.) \circ F) \subseteq ℝ$
15	2 14	sstrd	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ((.) \circ F)) \to A \subseteq ℝ$
16		eqid	$⊢ \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
17	16	ovolval	$⊢ A \subseteq ℝ \to {vol}^{} (A) = inf (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <)$
18	15 17	syl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ((.) \circ F)) \to {vol}^{} (A) = inf (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <)$
19		ssrab2	$⊢ \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} \subseteq ℝ^{*}$
20	16 1	elovolmr	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ((.) \circ F)) \to sup (ran S ℝ^{} <) \in \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <))\}$
21		infxrlb	$⊢ (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} \subseteq ℝ^{} \land sup (ran S ℝ^{} <) \in \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}) \to inf (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <) \leq sup (ran S ℝ^{} <)$
22	19 20 21	sylancr	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ((.) \circ F)) \to inf (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <) \leq sup (ran S ℝ^{} <)$
23	18 22	eqbrtrd	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ((.) \circ F)) \to {vol}^{} (A) \leq sup (ran S ℝ^{} <)$

Metamath Proof Explorer

Theorem ovollb

Proof