lt_card_ge_iff_apply_ge_of_antitone

English

If f is antitone, then for every j, j < card { i : a ≤ f(i) } iff a ≤ f(j).

Русский

Если f антитонична, то для каждого j верно: j < card{ i : a ≤ f(i) } эквивалентно a ≤ f(j).

LaTeX

$$$\\forall m\\, (f : \\mathrm{Fin}\,m \\to \\alpha)\\, (a \\in \\alpha),\\; \\mathrm{Antitone}(f) \\Rightarrow\\; j < \\mathrm{card}\\{ i : a \\le f(i) \\} \\iff a \\le f(j).$$$

Lean4

theorem lt_card_ge_iff_apply_ge_of_antitone [Preorder α] [DecidableLE α] {m : ℕ} (f : Fin m → α) (a : α)
    (h_sorted : Antitone f) (j : Fin m) : j < Fintype.card { i // a ≤ f i } ↔ a ≤ f j :=
  lt_card_le_iff_apply_le_of_monotone _ (OrderDual.toDual a) h_sorted.dual_right j

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