coverMincard_zero — Mathlib

English

If F is nonempty, then at level 0 the minimal cover has size 1: coverMincard T F 0 = 1.

Русский

Пусть F непусто; тогда при уровне 0 минимальное покрылие имеет размер 1: coverMincard T F 0 = 1.

LaTeX

$$$coverMincard(T,F,U,0) = 1$ (for F.Nonempty)$$

Lean4

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

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