netMaxcard_le_coverMincard — Mathlib

English

For symmetric U, netMaxcard T F U n ≤ coverMincard T F U n for all n.

Русский

При симметричном U выполняется неравенство netMaxcard T F U n ≤ coverMincard T F U n для всех n.

LaTeX

$$netMaxcard(T,F,U,n) \le coverMincard(T,F,U,n).$$

Lean4

theorem netMaxcard_le_coverMincard (T : X → X) (F : Set X) {U : Set (X × X)} (U_symm : IsSymmetricRel U) (n : ℕ) :
    netMaxcard T F U n ≤ coverMincard T F U n :=
  by
  rcases eq_top_or_lt_top (coverMincard T F U n) with h | h
  · exact h ▸ le_top
  · obtain ⟨t, t_cover, t_mincard⟩ := (coverMincard_finite_iff T F U n).1 h
    rw [← t_mincard]
    exact iSup₂_le fun s s_net ↦ Nat.cast_le.2 (s_net.card_le_card_of_isDynCoverOf U_symm t_cover)

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