exists_pos_measure_of_not_restrict_le_zero

English

If not v ≤_i 0, then there exists a measurable j ⊆ i with 0 < v(j).

Русский

Если не выполняется v ≤_i 0, существует измеримое j ⊆ i такое, что 0 < v(j).

LaTeX

$$¬(v ≤_i 0) ⇒ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < v(j)$$

Lean4

theorem exists_pos_measure_of_not_restrict_le_zero (hi : ¬v ≤[i] 0) : ∃ j : Set α, MeasurableSet j ∧ j ⊆ i ∧ 0 < v j :=
  by
  have hi₁ : MeasurableSet i := measurable_of_not_restrict_le_zero _ hi
  rw [restrict_le_restrict_iff _ _ hi₁] at hi
  push_neg at hi
  exact hi

Похожие утверждения