netMaxcard_antitone — Mathlib

English

The map U ↦ netMaxcard(T,F,U,n) is antitone: if U ⊆ V then netMaxcard(T,F,V,n) ≤ netMaxcard(T,F,U,n).

Русский

Отображение U ↦ netMaxcard(T,F,U,n) антимонотонно: U ⊆ V ⇒ netMaxcard(T,F,V,n) ≤ netMaxcard(T,F,U,n).

LaTeX

$$Antitone (fun U : Set (X × X) ↦ netMaxcard T F U n).$$

Lean4

theorem netMaxcard_antitone (T : X → X) (F : Set X) (n : ℕ) : Antitone fun U : Set (X × X) ↦ netMaxcard T F U n :=
  fun _ _ U_V ↦ biSup_mono fun _ h ↦ h.of_entourage_subset U_V

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