coverMincard_antitone — Mathlib

English

The mapping U ↦ coverMincard T F U n is antitone: if U ⊆ V then coverMincard T F U n ≥ coverMincard T F V n.

Русский

Отображение окружения по включению антонитно: если U ⊆ V, то coverMincard(T,F,U,n) ≥ coverMincard(T,F,V,n).

LaTeX

$$Antitone fun U => coverMincard T F U n$$

Lean4

theorem coverMincard_antitone (T : X → X) (F : Set X) (n : ℕ) : Antitone fun U : Set (X × X) ↦ coverMincard T F U n :=
  fun _ _ U_V ↦ biInf_mono fun _ h ↦ h.of_entourage_subset U_V

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