Home | Metamath
Proof Explorer Theorem List (p. 299 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | probtot 29801 | The probability of the universe set is 1. Second axiom of Kolmogorov. (Contributed by Thierry Arnoux, 8-Dec-2016.) |
⊢ (𝑃 ∈ Prob → (𝑃‘∪ dom 𝑃) = 1) | ||
Theorem | prob01 29802 | A probability is an element of [ 0 , 1 ]. First axiom of Kolmogorov. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃) → (𝑃‘𝐴) ∈ (0[,]1)) | ||
Theorem | probnul 29803 | The probability of the empty event set is 0. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ (𝑃 ∈ Prob → (𝑃‘∅) = 0) | ||
Theorem | unveldomd 29804 | The universe is an element of the domain of the probability, the universe (entire probability space) being ∪ dom 𝑃 in our construction. (Contributed by Thierry Arnoux, 22-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) ⇒ ⊢ (𝜑 → ∪ dom 𝑃 ∈ dom 𝑃) | ||
Theorem | unveldom 29805 | The universe is an element of the domain of the probability, the universe (entire probability space) being ∪ dom 𝑃 in our construction. (Contributed by Thierry Arnoux, 22-Jan-2017.) |
⊢ (𝑃 ∈ Prob → ∪ dom 𝑃 ∈ dom 𝑃) | ||
Theorem | nuleldmp 29806 | The empty set is an element of the domain of the probability. (Contributed by Thierry Arnoux, 22-Jan-2017.) |
⊢ (𝑃 ∈ Prob → ∅ ∈ dom 𝑃) | ||
Theorem | probcun 29807* | The probability of the union of a countable disjoint set of events is the sum of their probabilities. (Third axiom of Kolmogorov) Here, the Σ construct cannot be used as it can handle infinite indexing set only if they are subsets of ℤ, which is not the case here. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ 𝒫 dom 𝑃 ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥)) → (𝑃‘∪ 𝐴) = Σ*𝑥 ∈ 𝐴(𝑃‘𝑥)) | ||
Theorem | probun 29808 | The probability of the union two incompatible events is the sum of their probabilities. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → ((𝐴 ∩ 𝐵) = ∅ → (𝑃‘(𝐴 ∪ 𝐵)) = ((𝑃‘𝐴) + (𝑃‘𝐵)))) | ||
Theorem | probdif 29809 | The probability of the difference of two event sets. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → (𝑃‘(𝐴 ∖ 𝐵)) = ((𝑃‘𝐴) − (𝑃‘(𝐴 ∩ 𝐵)))) | ||
Theorem | probinc 29810 | A probability law is increasing with regard to event set inclusion. (Contributed by Thierry Arnoux, 10-Feb-2017.) |
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ 𝐴 ⊆ 𝐵) → (𝑃‘𝐴) ≤ (𝑃‘𝐵)) | ||
Theorem | probdsb 29811 | The probability of the complement of a set. That is, the probability that the event 𝐴 does not occur. (Contributed by Thierry Arnoux, 15-Dec-2016.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃) → (𝑃‘(∪ dom 𝑃 ∖ 𝐴)) = (1 − (𝑃‘𝐴))) | ||
Theorem | probmeasd 29812 | A probability measure is a measure. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) ⇒ ⊢ (𝜑 → 𝑃 ∈ ∪ ran measures) | ||
Theorem | probvalrnd 29813 | The value of a probability is a real number. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑃) ⇒ ⊢ (𝜑 → (𝑃‘𝐴) ∈ ℝ) | ||
Theorem | probtotrnd 29814 | The probability of the universe set is finite. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) ⇒ ⊢ (𝜑 → (𝑃‘∪ dom 𝑃) ∈ ℝ) | ||
Theorem | totprobd 29815* | Law of total probability, deduction form. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝒫 dom 𝑃) & ⊢ (𝜑 → ∪ 𝐵 = ∪ dom 𝑃) & ⊢ (𝜑 → 𝐵 ≼ ω) & ⊢ (𝜑 → Disj 𝑏 ∈ 𝐵 𝑏) ⇒ ⊢ (𝜑 → (𝑃‘𝐴) = Σ*𝑏 ∈ 𝐵(𝑃‘(𝑏 ∩ 𝐴))) | ||
Theorem | totprob 29816* | Law of total probability. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ (∪ 𝐵 = ∪ dom 𝑃 ∧ 𝐵 ∈ 𝒫 dom 𝑃 ∧ (𝐵 ≼ ω ∧ Disj 𝑏 ∈ 𝐵 𝑏))) → (𝑃‘𝐴) = Σ*𝑏 ∈ 𝐵(𝑃‘(𝑏 ∩ 𝐴))) | ||
Theorem | probfinmeasbOLD 29817* | Build a probability measure from a finite measure. (Contributed by Thierry Arnoux, 17-Dec-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝑀‘∪ 𝑆) ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 (𝑀‘∪ 𝑆))) ∈ Prob) | ||
Theorem | probfinmeasb 29818 | Build a probability measure from a finite measure. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝑀‘∪ 𝑆) ∈ ℝ+) → (𝑀∘𝑓/𝑐 /𝑒 (𝑀‘∪ 𝑆)) ∈ Prob) | ||
Theorem | probmeasb 29819* | Build a probability from a measure and a set with finite measure. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))) ∈ Prob) | ||
Syntax | ccprob 29820 | Extends class notation with the conditional probability builder. |
class cprob | ||
Definition | df-cndprob 29821* | Define the conditional probability. (Contributed by Thierry Arnoux, 14-Sep-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
⊢ cprob = (𝑝 ∈ Prob ↦ (𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏)))) | ||
Theorem | cndprobval 29822 | The value of the conditional probability , i.e. the probability for the event 𝐴, given 𝐵, under the probability law 𝑃. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → ((cprob‘𝑃)‘〈𝐴, 𝐵〉) = ((𝑃‘(𝐴 ∩ 𝐵)) / (𝑃‘𝐵))) | ||
Theorem | cndprobin 29823 | An identity linking conditional probability and intersection. (Contributed by Thierry Arnoux, 13-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑃‘𝐵) ≠ 0) → (((cprob‘𝑃)‘〈𝐴, 𝐵〉) · (𝑃‘𝐵)) = (𝑃‘(𝐴 ∩ 𝐵))) | ||
Theorem | cndprob01 29824 | The conditional probability has values in [0, 1]. (Contributed by Thierry Arnoux, 13-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑃‘𝐵) ≠ 0) → ((cprob‘𝑃)‘〈𝐴, 𝐵〉) ∈ (0[,]1)) | ||
Theorem | cndprobtot 29825 | The conditional probability given a certain event is one. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ (𝑃‘𝐴) ≠ 0) → ((cprob‘𝑃)‘〈∪ dom 𝑃, 𝐴〉) = 1) | ||
Theorem | cndprobnul 29826 | The conditional probability given empty event is zero. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ (𝑃‘𝐴) ≠ 0) → ((cprob‘𝑃)‘〈∅, 𝐴〉) = 0) | ||
Theorem | cndprobprob 29827* | The conditional probability defines a probability law. (Contributed by Thierry Arnoux, 23-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ∧ (𝑃‘𝐵) ≠ 0) → (𝑎 ∈ dom 𝑃 ↦ ((cprob‘𝑃)‘〈𝑎, 𝐵〉)) ∈ Prob) | ||
Theorem | bayesth 29828 | Bayes Theorem. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑃‘𝐴) ≠ 0 ∧ (𝑃‘𝐵) ≠ 0) → ((cprob‘𝑃)‘〈𝐴, 𝐵〉) = ((((cprob‘𝑃)‘〈𝐵, 𝐴〉) · (𝑃‘𝐴)) / (𝑃‘𝐵))) | ||
Syntax | crrv 29829 | Extend class notation with the class of real valued random variables. |
class rRndVar | ||
Definition | df-rrv 29830 | In its generic definition, a random variable is a measurable function from a probability space to a Borel set. Here, we specifically target real-valued random variables, i.e. measurable function from a probability space to the Borel sigma-algebra on the set of real numbers. (Contributed by Thierry Arnoux, 20-Sep-2016.) (Revised by Thierry Arnoux, 25-Jan-2017.) |
⊢ rRndVar = (𝑝 ∈ Prob ↦ (dom 𝑝MblFnM𝔅ℝ)) | ||
Theorem | rrvmbfm 29831 | A real-valued random variable is a measurable function from its sample space to the Borel sigma-algebra. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) ⇒ ⊢ (𝜑 → (𝑋 ∈ (rRndVar‘𝑃) ↔ 𝑋 ∈ (dom 𝑃MblFnM𝔅ℝ))) | ||
Theorem | isrrvv 29832* | Elementhood to the set of real-valued random variables with respect to the probability 𝑃. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) ⇒ ⊢ (𝜑 → (𝑋 ∈ (rRndVar‘𝑃) ↔ (𝑋:∪ dom 𝑃⟶ℝ ∧ ∀𝑦 ∈ 𝔅ℝ (◡𝑋 “ 𝑦) ∈ dom 𝑃))) | ||
Theorem | rrvvf 29833 | A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → 𝑋:∪ dom 𝑃⟶ℝ) | ||
Theorem | rrvfn 29834 | A real-valued random variable is a function over the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → 𝑋 Fn ∪ dom 𝑃) | ||
Theorem | rrvdm 29835 | The domain of a random variable is the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → dom 𝑋 = ∪ dom 𝑃) | ||
Theorem | rrvrnss 29836 | The range of a random variable as a subset of ℝ. (Contributed by Thierry Arnoux, 6-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → ran 𝑋 ⊆ ℝ) | ||
Theorem | rrvf2 29837 | A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → 𝑋:dom 𝑋⟶ℝ) | ||
Theorem | rrvdmss 29838 | The domain of a random variable. This is useful to shorten proofs. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → ∪ dom 𝑃 ⊆ dom 𝑋) | ||
Theorem | rrvfinvima 29839* | For a real-value random variable 𝑋, any open interval in ℝ is the image of a measurable set. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → ∀𝑦 ∈ 𝔅ℝ (◡𝑋 “ 𝑦) ∈ dom 𝑃) | ||
Theorem | 0rrv 29840* | The constant function equal to zero is a random variable. (Contributed by Thierry Arnoux, 16-Jan-2017.) (Revised by Thierry Arnoux, 30-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) ⇒ ⊢ (𝜑 → (𝑥 ∈ ∪ dom 𝑃 ↦ 0) ∈ (rRndVar‘𝑃)) | ||
Theorem | rrvadd 29841 | The sum of two random variables is a random variable. (Contributed by Thierry Arnoux, 4-Jun-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝑌 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → (𝑋 ∘𝑓 + 𝑌) ∈ (rRndVar‘𝑃)) | ||
Theorem | rrvmulc 29842 | A random variable multiplied by a constant is a random variable. (Contributed by Thierry Arnoux, 17-Jan-2017.) (Revised by Thierry Arnoux, 22-May-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑋∘𝑓/𝑐 · 𝐶) ∈ (rRndVar‘𝑃)) | ||
Theorem | rrvsum 29843 | An indexed sum of random variables is a random variable. (Contributed by Thierry Arnoux, 22-May-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋:ℕ⟶(rRndVar‘𝑃)) & ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑆 = (seq1( ∘𝑓 + , 𝑋)‘𝑁)) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑆 ∈ (rRndVar‘𝑃)) | ||
Syntax | corvc 29844 | Extend class notation to include the preimage set mapping operator. |
class ∘RV/𝑐𝑅 | ||
Definition | df-orvc 29845* |
Define the preimage set mapping operator. In probability theory, the
notation 𝑃(𝑋 = 𝐴) denotes the probability that a
random variable
𝑋 takes the value 𝐴. We
introduce here an operator which
enables to write this in Metamath as (𝑃‘(𝑋∘RV/𝑐 I 𝐴)), and
keep a similar notation. Because with this notation (𝑋∘RV/𝑐 I 𝐴)
is a set, we can also apply it to conditional probabilities, like in
(𝑃‘(𝑋∘RV/𝑐 I 𝐴) ∣ (𝑌∘RV/𝑐 I 𝐵))).
The oRVC operator transforms a relation 𝑅 into an operation taking a random variable 𝑋 and a constant 𝐶, and returning the preimage through 𝑋 of the equivalence class of 𝐶. The most commonly used relations are: - equality: {𝑋 = 𝐴} as (𝑋∘RV/𝑐 I 𝐴) cf. ideq 5196- elementhood: {𝑋 ∈ 𝐴} as (𝑋∘RV/𝑐 E 𝐴) cf. epel 4952- less-than: {𝑋 ≤ 𝐴} as (𝑋∘RV/𝑐 ≤ 𝐴) Even though it is primarily designed to be used within probability theory and with random variables, this operator is defined on generic functions, and could be used in other fields, e.g. for continuous functions. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
⊢ ∘RV/𝑐𝑅 = (𝑥 ∈ {𝑥 ∣ Fun 𝑥}, 𝑎 ∈ V ↦ (◡𝑥 “ {𝑦 ∣ 𝑦𝑅𝑎})) | ||
Theorem | orvcval 29846* | Value of the preimage mapping operator applied on a given random variable and constant. (Contributed by Thierry Arnoux, 19-Jan-2017.) |
⊢ (𝜑 → Fun 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) = (◡𝑋 “ {𝑦 ∣ 𝑦𝑅𝐴})) | ||
Theorem | orvcval2 29847* | Another way to express the value of the preimage mapping operator. (Contributed by Thierry Arnoux, 19-Jan-2017.) |
⊢ (𝜑 → Fun 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) = {𝑧 ∈ dom 𝑋 ∣ (𝑋‘𝑧)𝑅𝐴}) | ||
Theorem | elorvc 29848* | Elementhood of a preimage. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → Fun 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) ⇒ ⊢ ((𝜑 ∧ 𝑧 ∈ dom 𝑋) → (𝑧 ∈ (𝑋∘RV/𝑐𝑅𝐴) ↔ (𝑋‘𝑧)𝑅𝐴)) | ||
Theorem | orvcval4 29849* | The value of the preimage mapping operator can be restricted to preimages in the base set of the topology. Cf. orvcval 29846. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑋 ∈ (𝑆MblFnM(sigaGen‘𝐽))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) = (◡𝑋 “ {𝑦 ∈ ∪ 𝐽 ∣ 𝑦𝑅𝐴})) | ||
Theorem | orvcoel 29850* | If the relation produces open sets, preimage maps by a measurable function are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑋 ∈ (𝑆MblFnM(sigaGen‘𝐽))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → {𝑦 ∈ ∪ 𝐽 ∣ 𝑦𝑅𝐴} ∈ 𝐽) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) ∈ 𝑆) | ||
Theorem | orvccel 29851* | If the relation produces closed sets, preimage maps by a measurable function are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑋 ∈ (𝑆MblFnM(sigaGen‘𝐽))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → {𝑦 ∈ ∪ 𝐽 ∣ 𝑦𝑅𝐴} ∈ (Clsd‘𝐽)) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) ∈ 𝑆) | ||
Theorem | elorrvc 29852* | Elementhood of a preimage for a real-valued random variable. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ dom 𝑃) → (𝑧 ∈ (𝑋∘RV/𝑐𝑅𝐴) ↔ (𝑋‘𝑧)𝑅𝐴)) | ||
Theorem | orrvcval4 29853* | The value of the preimage mapping operator can be restricted to preimages of subsets of RR. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) = (◡𝑋 “ {𝑦 ∈ ℝ ∣ 𝑦𝑅𝐴})) | ||
Theorem | orrvcoel 29854* | If the relation produces open sets, preimage maps of a random variable are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → {𝑦 ∈ ℝ ∣ 𝑦𝑅𝐴} ∈ (topGen‘ran (,))) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) ∈ dom 𝑃) | ||
Theorem | orrvccel 29855* | If the relation produces closed sets, preimage maps are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → {𝑦 ∈ ℝ ∣ 𝑦𝑅𝐴} ∈ (Clsd‘(topGen‘ran (,)))) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) ∈ dom 𝑃) | ||
Theorem | orvcgteel 29856 | Preimage maps produced by the "greater than or equal" relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐◡ ≤ 𝐴) ∈ dom 𝑃) | ||
Theorem | orvcelval 29857 | Preimage maps produced by the membership relation. (Contributed by Thierry Arnoux, 6-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ 𝔅ℝ) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐 E 𝐴) = (◡𝑋 “ 𝐴)) | ||
Theorem | orvcelel 29858 | Preimage maps produced by the membership relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ 𝔅ℝ) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐 E 𝐴) ∈ dom 𝑃) | ||
Theorem | dstrvval 29859* | The value of the distribution of a random variable. (Contributed by Thierry Arnoux, 9-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐷 = (𝑎 ∈ 𝔅ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 E 𝑎)))) & ⊢ (𝜑 → 𝐴 ∈ 𝔅ℝ) ⇒ ⊢ (𝜑 → (𝐷‘𝐴) = (𝑃‘(◡𝑋 “ 𝐴))) | ||
Theorem | dstrvprob 29860* | The distribution of a random variable is a probability law. (TODO: could be shortened using dstrvval 29859) (Contributed by Thierry Arnoux, 10-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐷 = (𝑎 ∈ 𝔅ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 E 𝑎)))) ⇒ ⊢ (𝜑 → 𝐷 ∈ Prob) | ||
Theorem | orvclteel 29861 | Preimage maps produced by the "lower than or equal" relation are measurable sets. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐 ≤ 𝐴) ∈ dom 𝑃) | ||
Theorem | dstfrvel 29862 | Elementhood of preimage maps produced by the "lower than or equal" relation. (Contributed by Thierry Arnoux, 13-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ∪ dom 𝑃) & ⊢ (𝜑 → (𝑋‘𝐵) ≤ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝑋∘RV/𝑐 ≤ 𝐴)) | ||
Theorem | dstfrvunirn 29863* | The limit of all preimage maps by the "lower than or equal" relation is the universe. (Contributed by Thierry Arnoux, 12-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → ∪ ran (𝑛 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑛)) = ∪ dom 𝑃) | ||
Theorem | orvclteinc 29864 | Preimage maps produced by the "lower than or equal" relation are increasing. (Contributed by Thierry Arnoux, 11-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐 ≤ 𝐴) ⊆ (𝑋∘RV/𝑐 ≤ 𝐵)) | ||
Theorem | dstfrvinc 29865* | A cumulative distribution function is non-decreasing. (Contributed by Thierry Arnoux, 11-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥)))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) ≤ (𝐹‘𝐵)) | ||
Theorem | dstfrvclim1 29866* | The limit of the cumulative distribution function is one. (Contributed by Thierry Arnoux, 12-Feb-2017.) (Revised by Thierry Arnoux, 11-Jul-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥)))) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 1) | ||
Theorem | coinfliplem 29867 | Division in the extended real numbers can be used for the coin-flip example. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
⊢ 𝐻 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝐻 ≠ 𝑇 & ⊢ 𝑃 = ((# ↾ 𝒫 {𝐻, 𝑇})∘𝑓/𝑐 / 2) & ⊢ 𝑋 = {〈𝐻, 1〉, 〈𝑇, 0〉} ⇒ ⊢ 𝑃 = ((# ↾ 𝒫 {𝐻, 𝑇})∘𝑓/𝑐 /𝑒 2) | ||
Theorem | coinflipprob 29868 | The 𝑃 we defined for coin-flip is a probability law. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
⊢ 𝐻 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝐻 ≠ 𝑇 & ⊢ 𝑃 = ((# ↾ 𝒫 {𝐻, 𝑇})∘𝑓/𝑐 / 2) & ⊢ 𝑋 = {〈𝐻, 1〉, 〈𝑇, 0〉} ⇒ ⊢ 𝑃 ∈ Prob | ||
Theorem | coinflipspace 29869 | The space of our coin-flip probability. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
⊢ 𝐻 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝐻 ≠ 𝑇 & ⊢ 𝑃 = ((# ↾ 𝒫 {𝐻, 𝑇})∘𝑓/𝑐 / 2) & ⊢ 𝑋 = {〈𝐻, 1〉, 〈𝑇, 0〉} ⇒ ⊢ dom 𝑃 = 𝒫 {𝐻, 𝑇} | ||
Theorem | coinflipuniv 29870 | The universe of our coin-flip probability is {𝐻, 𝑇}. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
⊢ 𝐻 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝐻 ≠ 𝑇 & ⊢ 𝑃 = ((# ↾ 𝒫 {𝐻, 𝑇})∘𝑓/𝑐 / 2) & ⊢ 𝑋 = {〈𝐻, 1〉, 〈𝑇, 0〉} ⇒ ⊢ ∪ dom 𝑃 = {𝐻, 𝑇} | ||
Theorem | coinfliprv 29871 | The 𝑋 we defined for coin-flip is a random variable. (Contributed by Thierry Arnoux, 12-Jan-2017.) |
⊢ 𝐻 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝐻 ≠ 𝑇 & ⊢ 𝑃 = ((# ↾ 𝒫 {𝐻, 𝑇})∘𝑓/𝑐 / 2) & ⊢ 𝑋 = {〈𝐻, 1〉, 〈𝑇, 0〉} ⇒ ⊢ 𝑋 ∈ (rRndVar‘𝑃) | ||
Theorem | coinflippv 29872 | The probability of heads is one-half. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
⊢ 𝐻 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝐻 ≠ 𝑇 & ⊢ 𝑃 = ((# ↾ 𝒫 {𝐻, 𝑇})∘𝑓/𝑐 / 2) & ⊢ 𝑋 = {〈𝐻, 1〉, 〈𝑇, 0〉} ⇒ ⊢ (𝑃‘{𝐻}) = (1 / 2) | ||
Theorem | coinflippvt 29873 | The probability of tails is one-half. (Contributed by Thierry Arnoux, 5-Feb-2017.) |
⊢ 𝐻 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝐻 ≠ 𝑇 & ⊢ 𝑃 = ((# ↾ 𝒫 {𝐻, 𝑇})∘𝑓/𝑐 / 2) & ⊢ 𝑋 = {〈𝐻, 1〉, 〈𝑇, 0〉} ⇒ ⊢ (𝑃‘{𝑇}) = (1 / 2) | ||
Theorem | ballotlemoex 29874* | 𝑂 is a set. (Contributed by Thierry Arnoux, 7-Dec-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} ⇒ ⊢ 𝑂 ∈ V | ||
Theorem | ballotlem1 29875* | The size of the universe is a binomial coefficient. (Contributed by Thierry Arnoux, 23-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} ⇒ ⊢ (#‘𝑂) = ((𝑀 + 𝑁)C𝑀) | ||
Theorem | ballotlemelo 29876* | Elementhood in 𝑂. (Contributed by Thierry Arnoux, 17-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} ⇒ ⊢ (𝐶 ∈ 𝑂 ↔ (𝐶 ⊆ (1...(𝑀 + 𝑁)) ∧ (#‘𝐶) = 𝑀)) | ||
Theorem | ballotlem2 29877* | The probability that the first vote picked in a count is a B. (Contributed by Thierry Arnoux, 23-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) ⇒ ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁)) | ||
Theorem | ballotlemfval 29878* | The value of F. (Contributed by Thierry Arnoux, 23-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ (𝜑 → 𝐶 ∈ 𝑂) & ⊢ (𝜑 → 𝐽 ∈ ℤ) ⇒ ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) = ((#‘((1...𝐽) ∩ 𝐶)) − (#‘((1...𝐽) ∖ 𝐶)))) | ||
Theorem | ballotlemfelz 29879* | (𝐹‘𝐶) has values in ℤ. (Contributed by Thierry Arnoux, 23-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ (𝜑 → 𝐶 ∈ 𝑂) & ⊢ (𝜑 → 𝐽 ∈ ℤ) ⇒ ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℤ) | ||
Theorem | ballotlemfp1 29880* | If the 𝐽 th ballot is for A, (𝐹‘𝐶) goes up 1. If the 𝐽 th ballot is for B, (𝐹‘𝐶) goes down 1. (Contributed by Thierry Arnoux, 24-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ (𝜑 → 𝐶 ∈ 𝑂) & ⊢ (𝜑 → 𝐽 ∈ ℕ) ⇒ ⊢ (𝜑 → ((¬ 𝐽 ∈ 𝐶 → ((𝐹‘𝐶)‘𝐽) = (((𝐹‘𝐶)‘(𝐽 − 1)) − 1)) ∧ (𝐽 ∈ 𝐶 → ((𝐹‘𝐶)‘𝐽) = (((𝐹‘𝐶)‘(𝐽 − 1)) + 1)))) | ||
Theorem | ballotlemfc0 29881* | 𝐹 takes value 0 between negative and positive values. (Contributed by Thierry Arnoux, 24-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ (𝜑 → 𝐶 ∈ 𝑂) & ⊢ (𝜑 → 𝐽 ∈ ℕ) & ⊢ (𝜑 → ∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0) & ⊢ (𝜑 → 0 < ((𝐹‘𝐶)‘𝐽)) ⇒ ⊢ (𝜑 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0) | ||
Theorem | ballotlemfcc 29882* | 𝐹 takes value 0 between positive and negative values. (Contributed by Thierry Arnoux, 2-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ (𝜑 → 𝐶 ∈ 𝑂) & ⊢ (𝜑 → 𝐽 ∈ ℕ) & ⊢ (𝜑 → ∃𝑖 ∈ (1...𝐽)0 ≤ ((𝐹‘𝐶)‘𝑖)) & ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) < 0) ⇒ ⊢ (𝜑 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0) | ||
Theorem | ballotlemfmpn 29883* | (𝐹‘𝐶) finishes counting at (𝑀 − 𝑁). (Contributed by Thierry Arnoux, 25-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) ⇒ ⊢ (𝐶 ∈ 𝑂 → ((𝐹‘𝐶)‘(𝑀 + 𝑁)) = (𝑀 − 𝑁)) | ||
Theorem | ballotlemfval0 29884* | (𝐹‘𝐶) always starts counting at 0 . (Contributed by Thierry Arnoux, 25-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) ⇒ ⊢ (𝐶 ∈ 𝑂 → ((𝐹‘𝐶)‘0) = 0) | ||
Theorem | ballotleme 29885* | Elements of 𝐸. (Contributed by Thierry Arnoux, 14-Dec-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} ⇒ ⊢ (𝐶 ∈ 𝐸 ↔ (𝐶 ∈ 𝑂 ∧ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖))) | ||
Theorem | ballotlemodife 29886* | Elements of (𝑂 ∖ 𝐸). (Contributed by Thierry Arnoux, 7-Dec-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) ↔ (𝐶 ∈ 𝑂 ∧ ∃𝑖 ∈ (1...(𝑀 + 𝑁))((𝐹‘𝐶)‘𝑖) ≤ 0)) | ||
Theorem | ballotlem4 29887* | If the first pick is a vote for B, A is not ahead throughout the count. (Contributed by Thierry Arnoux, 25-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} ⇒ ⊢ (𝐶 ∈ 𝑂 → (¬ 1 ∈ 𝐶 → ¬ 𝐶 ∈ 𝐸)) | ||
Theorem | ballotlem5 29888* | If A is not ahead throughout, there is a 𝑘 where votes are tied. (Contributed by Thierry Arnoux, 1-Dec-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ∃𝑘 ∈ (1...(𝑀 + 𝑁))((𝐹‘𝐶)‘𝑘) = 0) | ||
Theorem | ballotlemi 29889* | Value of 𝐼 for a given counting 𝐶. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) = inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}, ℝ, < )) | ||
Theorem | ballotlemiex 29890* | Properties of (𝐼‘𝐶). (Contributed by Thierry Arnoux, 12-Dec-2016.) (Revised by AV, 6-Oct-2020.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) ∧ ((𝐹‘𝐶)‘(𝐼‘𝐶)) = 0)) | ||
Theorem | ballotlemi1 29891* | The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 12-Mar-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ ¬ 1 ∈ 𝐶) → (𝐼‘𝐶) ≠ 1) | ||
Theorem | ballotlemii 29892* | The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 4-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → (𝐼‘𝐶) ≠ 1) | ||
Theorem | ballotlemsup 29893* | The set of zeroes of 𝐹 satisfies the conditions to have a supremum. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ∃𝑧 ∈ ℝ (∀𝑤 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0} ¬ 𝑤 < 𝑧 ∧ ∀𝑤 ∈ ℝ (𝑧 < 𝑤 → ∃𝑦 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}𝑦 < 𝑤))) | ||
Theorem | ballotlemimin 29894* | (𝐼‘𝐶) is the first tie. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ¬ ∃𝑘 ∈ (1...((𝐼‘𝐶) − 1))((𝐹‘𝐶)‘𝑘) = 0) | ||
Theorem | ballotlemic 29895* | If the first vote is for B, the vote on the first tie is for A. (Contributed by Thierry Arnoux, 1-Dec-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ ¬ 1 ∈ 𝐶) → (𝐼‘𝐶) ∈ 𝐶) | ||
Theorem | ballotlem1c 29896* | If the first vote is for A, the vote on the first tie is for B. (Contributed by Thierry Arnoux, 4-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → ¬ (𝐼‘𝐶) ∈ 𝐶) | ||
Theorem | ballotlemsval 29897* | Value of 𝑆. (Contributed by Thierry Arnoux, 12-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑆‘𝐶) = (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝐶), (((𝐼‘𝐶) + 1) − 𝑖), 𝑖))) | ||
Theorem | ballotlemsv 29898* | Value of 𝑆 evaluated at 𝐽 for a given counting 𝐶. (Contributed by Thierry Arnoux, 12-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → ((𝑆‘𝐶)‘𝐽) = if(𝐽 ≤ (𝐼‘𝐶), (((𝐼‘𝐶) + 1) − 𝐽), 𝐽)) | ||
Theorem | ballotlemsgt1 29899* | 𝑆 maps values less than (𝐼‘𝐶) to values greater than 1. (Contributed by Thierry Arnoux, 28-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁)) ∧ 𝐽 < (𝐼‘𝐶)) → 1 < ((𝑆‘𝐶)‘𝐽)) | ||
Theorem | ballotlemsdom 29900* | Domain of 𝑆 for a given counting 𝐶. (Contributed by Thierry Arnoux, 12-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → ((𝑆‘𝐶)‘𝐽) ∈ (1...(𝑀 + 𝑁))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |