netMaxcard_zero — Mathlib

English

For any T and nonempty F, and any U, netMaxcard T F U 0 = 1.

Русский

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

LaTeX

$$netMaxcard(T,F,U,0)=1.$$

Lean4

theorem netMaxcard_zero (T : X → X) {F : Set X} (h : F.Nonempty) (U : Set (X × X)) : netMaxcard T F U 0 = 1 :=
  by
  apply (iSup₂_le _).antisymm ((one_le_netMaxcard_iff T F U 0).2 h)
  intro s ⟨_, s_net⟩
  simp only [ball, dynEntourage_zero, 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)

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