antitone_fun — Mathlib

English

Variant of antigen monotone transfer for SupIndep: if g dominates f pointwise, SupIndep g implies SupIndep f.

Русский

Вариант антимонотонности: если g доминирует f точечно, то SupIndep g ⇒ SupIndep f.

LaTeX

$$$(\\forall x \\in s, f(x) \\le g(x)) \\land (s.SupIndep g) \\Rightarrow (s.SupIndep f).$$$

Lean4

theorem antitone_fun {g : ι → α} (hle : ∀ x ∈ s, f x ≤ g x) (h : s.SupIndep g) : s.SupIndep f := fun _t hts i his hit ↦
  (h hts his hit).mono (hle i his) <| Finset.sup_mono_fun fun x hx ↦ hle x <| hts hx

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