Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
ht : s ⊆ t
this : IsProbabilityMeasure (condCount s)
⊢ ↑↑(condCount s) t = 1
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
ht : s ⊆ t
⊢ ↑↑(condCount s) t = 1
haveI := condCount_isProbabilityMeasure hs hs'
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
ht : s ⊆ t
this : IsProbabilityMeasure (condCount s)
⊢ ¬↑↑(condCount s) t < 1
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
ht : s ⊆ t
this : IsProbabilityMeasure (condCount s)
⊢ ↑↑(condCount s) t = 1
refine' eq_of_le_of_not_lt prob_le_one _
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
ht : s ⊆ t
this : IsProbabilityMeasure (condCount s)
⊢ ↑↑(condCount s) s ≤ ↑↑(condCount s) t
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
ht : s ⊆ t
this : IsProbabilityMeasure (condCount s)
⊢ ¬↑↑(condCount s) t < 1
rw [not_lt, ← condCount_self hs hs']
no goals
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
ht : s ⊆ t
this : IsProbabilityMeasure (condCount s)
⊢ ↑↑(condCount s) s ≤ ↑↑(condCount s) t
exact measure_mono ht