P. 344 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34301-34400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	omssubaddlem 34301*	For any small margin 𝐸, we can find a covering approaching the outer measure of a set 𝐴 by that margin. (Contributed by Thierry Arnoux, 18-Sep-2019.) (Revised by AV, 4-Oct-2020.)
⊢ 𝑀 = (toOMeas‘𝑅)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑄)    &   ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + 𝐸))
Theorem	omssubadd 34302*	A constructed outer measure is countably sub-additive. Lemma 1.5.4 of [Bogachev] p. 17. (Contributed by Thierry Arnoux, 21-Sep-2019.) (Revised by AV, 4-Oct-2020.)
⊢ 𝑀 = (toOMeas‘𝑅)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ⊆ ∪ 𝑄)    &   ⊢ (𝜑 → 𝑋 ≼ ω)    ⇒   ⊢ (𝜑 → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴))
Syntax	ccarsg 34303	Class declaration for the Caratheodory sigma-Algebra construction.
class toCaraSiga
Definition	df-carsg 34304*	Define a function constructing Caratheodory measurable sets for a given outer measure. See carsgval 34305 for its value. Definition 1.11.2 of [Bogachev] p. 41. (Contributed by Thierry Arnoux, 17-May-2020.)
⊢ toCaraSiga = (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)})
Theorem	carsgval 34305*	Value of the Caratheodory sigma-Algebra construction function. (Contributed by Thierry Arnoux, 17-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (toCaraSiga‘𝑀) = {𝑎 ∈ 𝒫 𝑂 ∣ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)})
Theorem	carsgcl 34306	Closure of the Caratheodory measurable sets. (Contributed by Thierry Arnoux, 17-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (toCaraSiga‘𝑀) ⊆ 𝒫 𝑂)
Theorem	elcarsg 34307*	Property of being a Caratheodory measurable set. (Contributed by Thierry Arnoux, 17-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (𝐴 ∈ (toCaraSiga‘𝑀) ↔ (𝐴 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ 𝐴))) = (𝑀‘𝑒))))
Theorem	baselcarsg 34308	The universe set, 𝑂, is Caratheodory measurable. (Contributed by Thierry Arnoux, 17-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑀‘∅) = 0)    ⇒   ⊢ (𝜑 → 𝑂 ∈ (toCaraSiga‘𝑀))
Theorem	0elcarsg 34309	The empty set is Caratheodory measurable. (Contributed by Thierry Arnoux, 30-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑀‘∅) = 0)    ⇒   ⊢ (𝜑 → ∅ ∈ (toCaraSiga‘𝑀))
Theorem	carsguni 34310	The union of all Caratheodory measurable sets is the universe. (Contributed by Thierry Arnoux, 22-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑀‘∅) = 0)    ⇒   ⊢ (𝜑 → ∪ (toCaraSiga‘𝑀) = 𝑂)
Theorem	elcarsgss 34311	Caratheodory measurable sets are subsets of the universe. (Contributed by Thierry Arnoux, 21-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ∈ (toCaraSiga‘𝑀))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝑂)
Theorem	difelcarsg 34312	The Caratheodory measurable sets are closed under complement. (Contributed by Thierry Arnoux, 17-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ∈ (toCaraSiga‘𝑀))    ⇒   ⊢ (𝜑 → (𝑂 ∖ 𝐴) ∈ (toCaraSiga‘𝑀))
Theorem	inelcarsg 34313*	The Caratheodory measurable sets are closed under intersection. (Contributed by Thierry Arnoux, 18-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ∈ (toCaraSiga‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝑂 ∧ 𝑏 ∈ 𝒫 𝑂) → (𝑀‘(𝑎 ∪ 𝑏)) ≤ ((𝑀‘𝑎) +𝑒 (𝑀‘𝑏)))    &   ⊢ (𝜑 → 𝐵 ∈ (toCaraSiga‘𝑀))    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ∈ (toCaraSiga‘𝑀))
Theorem	unelcarsg 34314*	The Caratheodory-measurable sets are closed under pairwise unions. (Contributed by Thierry Arnoux, 21-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ∈ (toCaraSiga‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝑂 ∧ 𝑏 ∈ 𝒫 𝑂) → (𝑀‘(𝑎 ∪ 𝑏)) ≤ ((𝑀‘𝑎) +𝑒 (𝑀‘𝑏)))    &   ⊢ (𝜑 → 𝐵 ∈ (toCaraSiga‘𝑀))    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ (toCaraSiga‘𝑀))
Theorem	difelcarsg2 34315*	The Caratheodory-measurable sets are closed under class difference. (Contributed by Thierry Arnoux, 30-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ∈ (toCaraSiga‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝑂 ∧ 𝑏 ∈ 𝒫 𝑂) → (𝑀‘(𝑎 ∪ 𝑏)) ≤ ((𝑀‘𝑎) +𝑒 (𝑀‘𝑏)))    &   ⊢ (𝜑 → 𝐵 ∈ (toCaraSiga‘𝑀))    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ (toCaraSiga‘𝑀))
Theorem	carsgmon 34316*	Utility lemma: Apply monotony. (Contributed by Thierry Arnoux, 29-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝑂)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦))    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ≤ (𝑀‘𝐵))
Theorem	carsgsigalem 34317*	Lemma for the following theorems. (Contributed by Thierry Arnoux, 23-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑀‘∅) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))    ⇒   ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂) → (𝑀‘(𝑒 ∪ 𝑓)) ≤ ((𝑀‘𝑒) +𝑒 (𝑀‘𝑓)))
Theorem	fiunelcarsg 34318*	The Caratheodory measurable sets are closed under finite union. (Contributed by Thierry Arnoux, 23-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑀‘∅) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀))    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ (toCaraSiga‘𝑀))
Theorem	carsgclctunlem1 34319*	Lemma for carsgclctun 34323. (Contributed by Thierry Arnoux, 23-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑀‘∅) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀))    &   ⊢ (𝜑 → Disj 𝑦 ∈ 𝐴 𝑦)    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑂)    ⇒   ⊢ (𝜑 → (𝑀‘(𝐸 ∩ ∪ 𝐴)) = Σ*𝑦 ∈ 𝐴(𝑀‘(𝐸 ∩ 𝑦)))
Theorem	carsggect 34320*	The outer measure is countably superadditive on Caratheodory measurable sets. (Contributed by Thierry Arnoux, 31-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑀‘∅) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))    &   ⊢ (𝜑 → ¬ ∅ ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≼ ω)    &   ⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀))    &   ⊢ (𝜑 → Disj 𝑦 ∈ 𝐴 𝑦)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦))    ⇒   ⊢ (𝜑 → Σ*𝑧 ∈ 𝐴(𝑀‘𝑧) ≤ (𝑀‘∪ 𝐴))
Theorem	carsgclctunlem2 34321*	Lemma for carsgclctun 34323. (Contributed by Thierry Arnoux, 25-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑀‘∅) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦))    &   ⊢ (𝜑 → Disj 𝑘 ∈ ℕ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (toCaraSiga‘𝑀))    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑂)    &   ⊢ (𝜑 → (𝑀‘𝐸) ≠ +∞)    ⇒   ⊢ (𝜑 → ((𝑀‘(𝐸 ∩ ∪ 𝑘 ∈ ℕ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴))) ≤ (𝑀‘𝐸))
Theorem	carsgclctunlem3 34322*	Lemma for carsgclctun 34323. (Contributed by Thierry Arnoux, 24-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑀‘∅) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦))    &   ⊢ (𝜑 → 𝐴 ≼ ω)    &   ⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀))    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑂)    ⇒   ⊢ (𝜑 → ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ≤ (𝑀‘𝐸))
Theorem	carsgclctun 34323*	The Caratheodory measurable sets are closed under countable union. (Contributed by Thierry Arnoux, 21-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑀‘∅) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦))    &   ⊢ (𝜑 → 𝐴 ≼ ω)    &   ⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀))    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ (toCaraSiga‘𝑀))
Theorem	carsgsiga 34324*	The Caratheodory measurable sets constructed from outer measures form a Sigma-algebra. Statement (iii) of Theorem 1.11.4 of [Bogachev] p. 42. (Contributed by Thierry Arnoux, 17-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑀‘∅) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦))    ⇒   ⊢ (𝜑 → (toCaraSiga‘𝑀) ∈ (sigAlgebra‘𝑂))
Theorem	omsmeas 34325	The restriction of a constructed outer measure to Caratheodory measurable sets is a measure. This theorem allows to construct measures from pre-measures with the required characteristics, as for the Lebesgue measure. (Contributed by Thierry Arnoux, 17-May-2020.)
⊢ 𝑀 = (toOMeas‘𝑅)    &   ⊢ 𝑆 = (toCaraSiga‘𝑀)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞))    &   ⊢ (𝜑 → ∅ ∈ dom 𝑅)    &   ⊢ (𝜑 → (𝑅‘∅) = 0)    ⇒   ⊢ (𝜑 → (𝑀 ↾ 𝑆) ∈ (measures‘𝑆))
Theorem	pmeasmono 34326*	This theorem's hypotheses define a pre-measure. A pre-measure is monotone. (Contributed by Thierry Arnoux, 19-Jul-2020.)
⊢ (𝜑 → 𝑃:𝑅⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑃‘∅) = 0)    &   ⊢ ((𝜑 ∧ (𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (𝑃‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑃‘𝑦))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑅)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑅)    &   ⊢ (𝜑 → (𝐵 ∖ 𝐴) ∈ 𝑅)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑃‘𝐴) ≤ (𝑃‘𝐵))
Theorem	pmeasadd 34327*	A premeasure on a ring of sets is additive on disjoint countable collections. This is called sigma-additivity. (Contributed by Thierry Arnoux, 19-Jul-2020.)
⊢ (𝜑 → 𝑃:𝑅⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑃‘∅) = 0)    &   ⊢ ((𝜑 ∧ (𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (𝑃‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑃‘𝑦))    &   ⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑅 ∈ 𝑄)    &   ⊢ (𝜑 → 𝐴 ≼ ω)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑅)    &   ⊢ (𝜑 → Disj 𝑘 ∈ 𝐴 𝐵)    ⇒   ⊢ (𝜑 → (𝑃‘∪ 𝑘 ∈ 𝐴 𝐵) = Σ*𝑘 ∈ 𝐴(𝑃‘𝐵))
21.3.19  Integration
21.3.19.1  Lebesgue integral - misc additions
Theorem	itgeq12dv 34328*	Equality theorem for an integral. (Contributed by Thierry Arnoux, 14-Feb-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑥)
21.3.19.2  Bochner integral
Syntax	citgm 34329	Extend class notation with the (measure) Bochner integral.
class itgm
Syntax	csitm 34330	Extend class notation with the integral metric for simple functions.
class sitm
Syntax	csitg 34331	Extend class notation with the integral of simple functions.
class sitg
Definition	df-sitg 34332*	Define the integral of simple functions from a measurable space dom 𝑚 to a generic space 𝑤 equipped with the right scalar product. 𝑤 will later be required to be a Banach space. These simple functions are required to take finitely many different values: this is expressed by ran 𝑔 ∈ Fin in the definition. Moreover, for each 𝑥, the pre-image (◡𝑔 “ {𝑥}) is requested to be measurable, of finite measure. In this definition, (sigaGen‘(TopOpen‘𝑤)) is the Borel sigma-algebra on 𝑤, and the functions 𝑔 range over the measurable functions over that Borel algebra. Definition 2.4.1 of [Bogachev] p. 118. (Contributed by Thierry Arnoux, 21-Oct-2017.)
⊢ sitg = (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥)))))
Definition	df-sitm 34333*	Define the integral metric for simple functions, as the integral of the distances between the function values. Since distances take nonnegative values in ℝ*, the range structure for this integral is (ℝ*𝑠 ↾s (0[,]+∞)). See definition 2.3.1 of [Bogachev] p. 116. (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ sitm = (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ dom (𝑤sitg𝑚), 𝑔 ∈ dom (𝑤sitg𝑚) ↦ (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑤)𝑔))))
Theorem	sitgval 34334*	Value of the simple function integral builder for a given space 𝑊 and measure 𝑀. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (sigaGen‘𝐽)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    ⇒   ⊢ (𝜑 → (𝑊sitg𝑀) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))))
Theorem	issibf 34335*	The predicate "𝐹 is a simple function" relative to the Bochner integral. (Contributed by Thierry Arnoux, 19-Feb-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (sigaGen‘𝐽)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom (𝑊sitg𝑀) ↔ (𝐹 ∈ (dom 𝑀MblFnM𝑆) ∧ ran 𝐹 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝐹 ∖ { 0 })(𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞))))
Theorem	sibf0 34336	The constant zero function is a simple function. (Contributed by Thierry Arnoux, 4-Mar-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (sigaGen‘𝐽)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝑊 ∈ TopSp)    &   ⊢ (𝜑 → 𝑊 ∈ Mnd)    ⇒   ⊢ (𝜑 → (∪ dom 𝑀 × { 0 }) ∈ dom (𝑊sitg𝑀))
Theorem	sibfmbl 34337	A simple function is measurable. (Contributed by Thierry Arnoux, 19-Feb-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (sigaGen‘𝐽)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (dom 𝑀MblFnM𝑆))
Theorem	sibff 34338	A simple function is a function. (Contributed by Thierry Arnoux, 19-Feb-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (sigaGen‘𝐽)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))    ⇒   ⊢ (𝜑 → 𝐹:∪ dom 𝑀⟶∪ 𝐽)
Theorem	sibfrn 34339	A simple function has finite range. (Contributed by Thierry Arnoux, 19-Feb-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (sigaGen‘𝐽)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))    ⇒   ⊢ (𝜑 → ran 𝐹 ∈ Fin)
Theorem	sibfima 34340	Any preimage of a singleton by a simple function is measurable. (Contributed by Thierry Arnoux, 19-Feb-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (sigaGen‘𝐽)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ (ran 𝐹 ∖ { 0 })) → (𝑀‘(◡𝐹 “ {𝐴})) ∈ (0[,)+∞))
Theorem	sibfinima 34341	The measure of the intersection of any two preimages by simple functions is a real number. (Contributed by Thierry Arnoux, 21-Mar-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (sigaGen‘𝐽)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))    &   ⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀))    &   ⊢ (𝜑 → 𝑊 ∈ TopSp)    &   ⊢ (𝜑 → 𝐽 ∈ Fre)    ⇒   ⊢ (((𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺) ∧ (𝑋 ≠ 0 ∨ 𝑌 ≠ 0 )) → (𝑀‘((◡𝐹 “ {𝑋}) ∩ (◡𝐺 “ {𝑌}))) ∈ (0[,)+∞))
Theorem	sibfof 34342	Applying function operations on simple functions results in simple functions with regard to the destination space, provided the operation fulfills a simple condition. (Contributed by Thierry Arnoux, 12-Mar-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (sigaGen‘𝐽)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))    &   ⊢ 𝐶 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝑊 ∈ TopSp)    &   ⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶)    &   ⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀))    &   ⊢ (𝜑 → 𝐾 ∈ TopSp)    &   ⊢ (𝜑 → 𝐽 ∈ Fre)    &   ⊢ (𝜑 → ( 0 + 0 ) = (0g‘𝐾))    ⇒   ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ dom (𝐾sitg𝑀))
Theorem	sitgfval 34343*	Value of the Bochner integral for a simple function 𝐹. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (sigaGen‘𝐽)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))    ⇒   ⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) = (𝑊 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥))))
Theorem	sitgclg 34344*	Closure of the Bochner integral on simple functions, generic version. See sitgclbn 34345 for the version for Banach spaces. (Contributed by Thierry Arnoux, 24-Feb-2018.) (Proof shortened by AV, 12-Dec-2019.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (sigaGen‘𝐽)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))    &   ⊢ 𝐺 = (Scalar‘𝑊)    &   ⊢ 𝐷 = ((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))    &   ⊢ (𝜑 → 𝑊 ∈ TopSp)    &   ⊢ (𝜑 → 𝑊 ∈ CMnd)    &   ⊢ (𝜑 → (Scalar‘𝑊) ∈ ℝExt )    &   ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → (𝑚 · 𝑥) ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) ∈ 𝐵)
Theorem	sitgclbn 34345	Closure of the Bochner integral on a simple function. This version is specific to Banach spaces, with additional conditions on its scalar field. (Contributed by Thierry Arnoux, 24-Feb-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (sigaGen‘𝐽)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))    &   ⊢ (𝜑 → 𝑊 ∈ Ban)    &   ⊢ (𝜑 → (Scalar‘𝑊) ∈ ℝExt )    ⇒   ⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) ∈ 𝐵)
Theorem	sitgclcn 34346	Closure of the Bochner integral on a simple function. This version is specific to Banach spaces on the complex numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (sigaGen‘𝐽)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))    &   ⊢ (𝜑 → 𝑊 ∈ Ban)    &   ⊢ (𝜑 → (Scalar‘𝑊) = ℂfld)    ⇒   ⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) ∈ 𝐵)
Theorem	sitgclre 34347	Closure of the Bochner integral on a simple function. This version is specific to Banach spaces on the real numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (sigaGen‘𝐽)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))    &   ⊢ (𝜑 → 𝑊 ∈ Ban)    &   ⊢ (𝜑 → (Scalar‘𝑊) = ℝfld)    ⇒   ⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) ∈ 𝐵)
Theorem	sitg0 34348	The integral of the constant zero function is zero. (Contributed by Thierry Arnoux, 13-Mar-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (sigaGen‘𝐽)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝑊 ∈ TopSp)    &   ⊢ (𝜑 → 𝑊 ∈ Mnd)    ⇒   ⊢ (𝜑 → ((𝑊sitg𝑀)‘(∪ dom 𝑀 × { 0 })) = 0 )
Theorem	sitgf 34349*	The integral for simple functions is itself a function. (Contributed by Thierry Arnoux, 13-Feb-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (sigaGen‘𝐽)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ dom (𝑊sitg𝑀)) → ((𝑊sitg𝑀)‘𝑓) ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑊sitg𝑀):dom (𝑊sitg𝑀)⟶𝐵)
Theorem	sitgaddlemb 34350	Lemma for * sitgadd . (Contributed by Thierry Arnoux, 10-Mar-2019.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝑆 = (sigaGen‘𝐽)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝑊 ∈ TopSp)    &   ⊢ (𝜑 → (𝑊 ↾v (𝐻 “ (0[,)+∞))) ∈ SLMod)    &   ⊢ (𝜑 → 𝐽 ∈ Fre)    &   ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))    &   ⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀))    &   ⊢ (𝜑 → (Scalar‘𝑊) ∈ ℝExt )    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → ((𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) · (2nd ‘𝑝)) ∈ 𝐵)
Theorem	sitmval 34351*	Value of the simple function integral metric for a given space 𝑊 and measure 𝑀. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐷 = (dist‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    ⇒   ⊢ (𝜑 → (𝑊sitm𝑀) = (𝑓 ∈ dom (𝑊sitg𝑀), 𝑔 ∈ dom (𝑊sitg𝑀) ↦ (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑀)‘(𝑓 ∘f 𝐷𝑔))))
Theorem	sitmfval 34352	Value of the integral distance between two simple functions. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐷 = (dist‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))    &   ⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀))    ⇒   ⊢ (𝜑 → (𝐹(𝑊sitm𝑀)𝐺) = (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑀)‘(𝐹 ∘f 𝐷𝐺)))
Theorem	sitmcl 34353	Closure of the integral distance between two simple functions, for an extended metric space. (Contributed by Thierry Arnoux, 13-Feb-2018.)
⊢ (𝜑 → 𝑊 ∈ Mnd)    &   ⊢ (𝜑 → 𝑊 ∈ ∞MetSp)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))    &   ⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀))    ⇒   ⊢ (𝜑 → (𝐹(𝑊sitm𝑀)𝐺) ∈ (0[,]+∞))
Theorem	sitmf 34354	The integral metric as a function. (Contributed by Thierry Arnoux, 13-Mar-2018.)
⊢ (𝜑 → 𝑊 ∈ Mnd)    &   ⊢ (𝜑 → 𝑊 ∈ ∞MetSp)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    ⇒   ⊢ (𝜑 → (𝑊sitm𝑀):(dom (𝑊sitg𝑀) × dom (𝑊sitg𝑀))⟶(0[,]+∞))
Definition	df-itgm 34355*	Define the Bochner integral as the extension by continuity of the Bochnel integral for simple functions. Bogachev first defines 'fundamental in the mean' sequences, in definition 2.3.1 of [Bogachev] p. 116, and notes that those are actually Cauchy sequences for the pseudometric (𝑤sitm𝑚). He then defines the Bochner integral in chapter 2.4.4 in [Bogachev] p. 118. The definition of the Lebesgue integral, df-itg 25658. (Contributed by Thierry Arnoux, 13-Feb-2018.)
⊢ itgm = (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (((metUnif‘(𝑤sitm𝑚))CnExt(UnifSt‘𝑤))‘(𝑤sitg𝑚)))
21.3.20  Euler's partition theorem
Theorem	oddpwdc 34356*	Lemma for eulerpart 34384. The function 𝐹 that decomposes a number into its "odd" and "even" parts, which is to say the largest power of two and largest odd divisor of a number, is a bijection from pairs of a nonnegative integer and an odd number to positive integers. (Contributed by Thierry Arnoux, 15-Aug-2017.)
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    ⇒   ⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ
Theorem	oddpwdcv 34357*	Lemma for eulerpart 34384: value of the 𝐹 function. (Contributed by Thierry Arnoux, 9-Sep-2017.)
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    ⇒   ⊢ (𝑊 ∈ (𝐽 × ℕ0) → (𝐹‘𝑊) = ((2↑(2nd ‘𝑊)) · (1st ‘𝑊)))
Theorem	eulerpartlemsv1 34358*	Lemma for eulerpart 34384. Value of the sum of a partition 𝐴. (Contributed by Thierry Arnoux, 26-Aug-2018.)
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))    ⇒   ⊢ (𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ ℕ ((𝐴‘𝑘) · 𝑘))
Theorem	eulerpartlemelr 34359*	Lemma for eulerpart 34384. (Contributed by Thierry Arnoux, 8-Aug-2018.)
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))    ⇒   ⊢ (𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) → (𝐴:ℕ⟶ℕ0 ∧ (◡𝐴 “ ℕ) ∈ Fin))
Theorem	eulerpartlemsv2 34360*	Lemma for eulerpart 34384. Value of the sum of a finite partition 𝐴 (Contributed by Thierry Arnoux, 19-Aug-2018.)
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))    ⇒   ⊢ (𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘))
Theorem	eulerpartlemsf 34361*	Lemma for eulerpart 34384. (Contributed by Thierry Arnoux, 8-Aug-2018.)
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))    ⇒   ⊢ 𝑆:((ℕ0 ↑m ℕ) ∩ 𝑅)⟶ℕ0
Theorem	eulerpartlems 34362*	Lemma for eulerpart 34384. (Contributed by Thierry Arnoux, 6-Aug-2018.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))    ⇒   ⊢ ((𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ∧ 𝑡 ∈ (ℤ≥‘((𝑆‘𝐴) + 1))) → (𝐴‘𝑡) = 0)
Theorem	eulerpartlemsv3 34363*	Lemma for eulerpart 34384. Value of the sum of a finite partition 𝐴 (Contributed by Thierry Arnoux, 19-Aug-2018.)
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))    ⇒   ⊢ (𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (1...(𝑆‘𝐴))((𝐴‘𝑘) · 𝑘))
Theorem	eulerpartlemgc 34364*	Lemma for eulerpart 34384. (Contributed by Thierry Arnoux, 9-Aug-2018.)
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))    ⇒   ⊢ ((𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ∧ (𝑡 ∈ ℕ ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → ((2↑𝑛) · 𝑡) ≤ (𝑆‘𝐴))
Theorem	eulerpartleme 34365*	Lemma for eulerpart 34384. (Contributed by Mario Carneiro, 26-Jan-2015.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    ⇒   ⊢ (𝐴 ∈ 𝑃 ↔ (𝐴:ℕ⟶ℕ0 ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝐴‘𝑘) · 𝑘) = 𝑁))
Theorem	eulerpartlemv 34366*	Lemma for eulerpart 34384. (Contributed by Thierry Arnoux, 19-Aug-2018.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    ⇒   ⊢ (𝐴 ∈ 𝑃 ↔ (𝐴:ℕ⟶ℕ0 ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = 𝑁))
Theorem	eulerpartlemo 34367*	Lemma for eulerpart 34384: 𝑂 is the set of odd partitions of 𝑁. (Contributed by Thierry Arnoux, 10-Aug-2017.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    ⇒   ⊢ (𝐴 ∈ 𝑂 ↔ (𝐴 ∈ 𝑃 ∧ ∀𝑛 ∈ (◡𝐴 “ ℕ) ¬ 2 ∥ 𝑛))
Theorem	eulerpartlemd 34368*	Lemma for eulerpart 34384: 𝐷 is the set of distinct part. of 𝑁. (Contributed by Thierry Arnoux, 11-Aug-2017.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    ⇒   ⊢ (𝐴 ∈ 𝐷 ↔ (𝐴 ∈ 𝑃 ∧ (𝐴 “ ℕ) ⊆ {0, 1}))
Theorem	eulerpartlem1 34369*	Lemma for eulerpart 34384. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    ⇒   ⊢ 𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
Theorem	eulerpartlemb 34370*	Lemma for eulerpart 34384. The set of all partitions of 𝑁 is finite. (Contributed by Mario Carneiro, 26-Jan-2015.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    ⇒   ⊢ 𝑃 ∈ Fin
Theorem	eulerpartlemt0 34371*	Lemma for eulerpart 34384. (Contributed by Thierry Arnoux, 19-Sep-2017.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    ⇒   ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) ↔ (𝐴 ∈ (ℕ0 ↑m ℕ) ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ (◡𝐴 “ ℕ) ⊆ 𝐽))
Theorem	eulerpartlemf 34372*	Lemma for eulerpart 34384: Odd partitions are zero for even numbers. (Contributed by Thierry Arnoux, 9-Sep-2017.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    ⇒   ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → (𝐴‘𝑡) = 0)
Theorem	eulerpartlemt 34373*	Lemma for eulerpart 34384. (Contributed by Thierry Arnoux, 19-Sep-2017.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    ⇒   ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))
Theorem	eulerpartgbij 34374*	Lemma for eulerpart 34384: The 𝐺 function is a bijection. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    ⇒   ⊢ 𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)
Theorem	eulerpartlemgv 34375*	Lemma for eulerpart 34384: value of the function 𝐺. (Contributed by Thierry Arnoux, 13-Nov-2017.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    ⇒   ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))))))
Theorem	eulerpartlemr 34376*	Lemma for eulerpart 34384. (Contributed by Thierry Arnoux, 13-Nov-2017.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    ⇒   ⊢ 𝑂 = ((𝑇 ∩ 𝑅) ∩ 𝑃)
Theorem	eulerpartlemmf 34377*	Lemma for eulerpart 34384. (Contributed by Thierry Arnoux, 30-Aug-2018.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    ⇒   ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (bits ∘ (𝐴 ↾ 𝐽)) ∈ 𝐻)
Theorem	eulerpartlemgvv 34378*	Lemma for eulerpart 34384: value of the function 𝐺 evaluated. (Contributed by Thierry Arnoux, 10-Aug-2018.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    ⇒   ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → ((𝐺‘𝐴)‘𝐵) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵, 1, 0))
Theorem	eulerpartlemgu 34379*	Lemma for eulerpart 34384: Rewriting the 𝑈 set for an odd partition Note that interestingly, this proof reuses marypha2lem2 9476. (Contributed by Thierry Arnoux, 10-Aug-2018.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    &   ⊢ 𝑈 = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))    ⇒   ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝑈 = {⟨𝑡, 𝑛⟩ ∣ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ ((bits ∘ 𝐴)‘𝑡))})
Theorem	eulerpartlemgh 34380*	Lemma for eulerpart 34384: The 𝐹 function is a bijection on the 𝑈 subsets. (Contributed by Thierry Arnoux, 15-Aug-2018.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    &   ⊢ 𝑈 = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))    ⇒   ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐹 ↾ 𝑈):𝑈–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})
Theorem	eulerpartlemgf 34381*	Lemma for eulerpart 34384: Images under 𝐺 have finite support. (Contributed by Thierry Arnoux, 29-Aug-2018.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    ⇒   ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡(𝐺‘𝐴) “ ℕ) ∈ Fin)
Theorem	eulerpartlemgs2 34382*	Lemma for eulerpart 34384: The 𝐺 function also preserves partition sums. (Contributed by Thierry Arnoux, 10-Sep-2017.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    &   ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))    ⇒   ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = (𝑆‘𝐴))
Theorem	eulerpartlemn 34383*	Lemma for eulerpart 34384. (Contributed by Thierry Arnoux, 30-Aug-2018.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    &   ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))    ⇒   ⊢ (𝐺 ↾ 𝑂):𝑂–1-1-onto→𝐷
Theorem	eulerpart 34384*	Euler's theorem on partitions, also known as a special case of Glaisher's theorem. Let 𝑃 be the set of all partitions of 𝑁, represented as multisets of positive integers, which is to say functions from ℕ to ℕ0 where the value of the function represents the number of repetitions of an individual element, and the sum of all the elements with repetition equals 𝑁. Then the set 𝑂 of all partitions that only consist of odd numbers and the set 𝐷 of all partitions which have no repeated elements have the same cardinality. This is Metamath 100 proof #45. (Contributed by Thierry Arnoux, 14-Aug-2018.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    ⇒   ⊢ (♯‘𝑂) = (♯‘𝐷)
21.3.21  Sequences defined by strong recursion
Syntax	csseq 34385	Sequences defined by strong recursion.
class seqstr
Definition	df-sseq 34386*	Define a builder for sequences by strong recursion, i.e., by computing the value of the n-th element of the sequence from all preceding elements and not just the previous one. (Contributed by Thierry Arnoux, 21-Apr-2019.)
⊢ seqstr = (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ (lastS ∘ seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓‘𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓‘𝑚)”⟩)})))))
Theorem	subiwrd 34387	Lemma for sseqp1 34397. (Contributed by Thierry Arnoux, 25-Apr-2019.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝐹:ℕ0⟶𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)) ∈ Word 𝑆)
Theorem	subiwrdlen 34388	Length of a subword of an infinite word. (Contributed by Thierry Arnoux, 25-Apr-2019.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝐹:ℕ0⟶𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (♯‘(𝐹 ↾ (0..^𝑁))) = 𝑁)
Theorem	iwrdsplit 34389	Lemma for sseqp1 34397. (Contributed by Thierry Arnoux, 25-Apr-2019.) (Proof shortened by AV, 14-Oct-2022.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝐹:ℕ0⟶𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐹 ↾ (0..^(𝑁 + 1))) = ((𝐹 ↾ (0..^𝑁)) ++ ⟨“(𝐹‘𝑁)”⟩))
Theorem	sseqval 34390*	Value of the strong sequence builder function. The set 𝑊 represents here the words of length greater than or equal to the lenght of the initial sequence 𝑀. (Contributed by Thierry Arnoux, 21-Apr-2019.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ Word 𝑆)    &   ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀))))    &   ⊢ (𝜑 → 𝐹:𝑊⟶𝑆)    ⇒   ⊢ (𝜑 → (𝑀seqstr𝐹) = (𝑀 ∪ (lastS ∘ seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})))))
Theorem	sseqfv1 34391	Value of the strong sequence builder function at one of its initial values. (Contributed by Thierry Arnoux, 21-Apr-2019.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ Word 𝑆)    &   ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀))))    &   ⊢ (𝜑 → 𝐹:𝑊⟶𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝑀)))    ⇒   ⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = (𝑀‘𝑁))
Theorem	sseqfn 34392	A strong recursive sequence is a function over the nonnegative integers. (Contributed by Thierry Arnoux, 23-Apr-2019.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ Word 𝑆)    &   ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀))))    &   ⊢ (𝜑 → 𝐹:𝑊⟶𝑆)    ⇒   ⊢ (𝜑 → (𝑀seqstr𝐹) Fn ℕ0)
Theorem	sseqmw 34393	Lemma for sseqf 34394 amd sseqp1 34397. (Contributed by Thierry Arnoux, 25-Apr-2019.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ Word 𝑆)    &   ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀))))    &   ⊢ (𝜑 → 𝐹:𝑊⟶𝑆)    ⇒   ⊢ (𝜑 → 𝑀 ∈ 𝑊)
Theorem	sseqf 34394	A strong recursive sequence is a function over the nonnegative integers. (Contributed by Thierry Arnoux, 23-Apr-2019.) (Proof shortened by AV, 7-Mar-2022.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ Word 𝑆)    &   ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀))))    &   ⊢ (𝜑 → 𝐹:𝑊⟶𝑆)    ⇒   ⊢ (𝜑 → (𝑀seqstr𝐹):ℕ0⟶𝑆)
Theorem	sseqfres 34395	The first elements in the strong recursive sequence are the sequence initializer. (Contributed by Thierry Arnoux, 23-Apr-2019.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ Word 𝑆)    &   ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀))))    &   ⊢ (𝜑 → 𝐹:𝑊⟶𝑆)    ⇒   ⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))) = 𝑀)
Theorem	sseqfv2 34396*	Value of the strong sequence builder function. (Contributed by Thierry Arnoux, 21-Apr-2019.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ Word 𝑆)    &   ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀))))    &   ⊢ (𝜑 → 𝐹:𝑊⟶𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(♯‘𝑀)))    ⇒   ⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = (lastS‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑁)))
Theorem	sseqp1 34397	Value of the strong sequence builder function at a successor. (Contributed by Thierry Arnoux, 24-Apr-2019.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ Word 𝑆)    &   ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀))))    &   ⊢ (𝜑 → 𝐹:𝑊⟶𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(♯‘𝑀)))    ⇒   ⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁))))
21.3.22  Fibonacci Numbers
Syntax	cfib 34398	The Fibonacci sequence.
class Fibci
Definition	df-fib 34399	Define the Fibonacci sequence, where that each element is the sum of the two preceding ones, starting from 0 and 1. (Contributed by Thierry Arnoux, 25-Apr-2019.)
⊢ Fibci = (⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (◡♯ “ (ℤ≥‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))))
Theorem	fiblem 34400	Lemma for fib0 34401, fib1 34402 and fibp1 34403. (Contributed by Thierry Arnoux, 25-Apr-2019.)
⊢ (𝑤 ∈ (Word ℕ0 ∩ (◡♯ “ (ℤ≥‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))):(Word ℕ0 ∩ (◡♯ “ (ℤ≥‘(♯‘⟨“01”⟩))))⟶ℕ0