netMaxcard_univ — Mathlib

English

For any nonempty F, and any n, netMaxcard T F Set.univ n = 1.

Русский

Для любого непустого F и любого n, netMaxcard T F Set.univ n = 1.

LaTeX

$$netMaxcard(T,F,Set.univ,n)=1.$$

Lean4

theorem netMaxcard_univ (T : X → X) {F : Set X} (h : F.Nonempty) (n : ℕ) : netMaxcard T F univ n = 1 :=
  by
  apply (iSup₂_le _).antisymm ((one_le_netMaxcard_iff T F univ n).2 h)
  intro s ⟨_, s_net⟩
  simp only [ball, dynEntourage_univ, preimage_univ] at s_net
  norm_cast
  refine Finset.card_le_one.2 fun x x_s y y_s ↦ ?_
  exact PairwiseDisjoint.elim_set s_net x_s y_s x (mem_univ x) (mem_univ x)

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