netMaxcard_empty — Mathlib

English

If F is empty, then netMaxcard T F ∅ U n = 0 (i.e., the maximum size is zero).

Русский

Если F пусто, то netMaxcard T F ∅ U n = 0 (максимальная кардинальность равна нулю).

LaTeX

$$netMaxcard(T,\emptyset,U,n) = 0.$$

Lean4

@[simp]
theorem netMaxcard_empty {T : X → X} {U : Set (X × X)} {n : ℕ} : netMaxcard T ∅ U n = 0 :=
  by
  rw [netMaxcard, ← bot_eq_zero, iSup₂_eq_bot]
  intro s s_net
  replace s_net := subset_empty_iff.1 s_net.1
  norm_cast at s_net
  rw [s_net, Finset.card_empty, CharP.cast_eq_zero, bot_eq_zero']

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