coverMincard_univ — Mathlib

English

If the set F is nonempty, then the coverMincard on the entire space with the universal relation is 1 for any n: coverMincard T F univ n = 1.

Русский

Если F непусто, то для всей области пространства и всеобъемлющей связи значеение coverMincard равно 1 для любых n.

LaTeX

$$$coverMincard(T,F,\univ,n)=1$$$

Lean4

theorem coverMincard_univ (T : X → X) {F : Set X} (h : F.Nonempty) (n : ℕ) : coverMincard T F univ n = 1 :=
  by
  apply le_antisymm _ ((one_le_coverMincard_iff T F univ n).2 h)
  obtain ⟨x, _⟩ := h
  have := isDynCoverOf_univ T F n (singleton_nonempty x)
  rw [← Finset.coe_singleton] at this
  apply this.coverMincard_le_card.trans_eq
  rw [Finset.card_singleton, Nat.cast_one]

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