exists_lt_of_lt_expect — Mathlib

English

If there exists a nonempty s with a lower bound a exceeding the average, then there is an element in s exceeding a.

Русский

Если существует непустое s с нижней границей, превосходящей среднее, то найдётся элемент в s, превышающий её.

LaTeX

$$$\\exists x\\in s, a < f(x) \\Rightarrow \\exists x\\in s, a < f(x)$$$

Lean4

theorem exists_lt_of_lt_expect (hs : s.Nonempty) (h : a < 𝔼 i ∈ s, f i) : ∃ x ∈ s, a < f x := by contrapose! h;
  exact expect_le hs h

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