instGradeMinOrder_nat — Mathlib

English

There is a grading from natural numbers to Finset α such that if s is minimal, then its card is minimal in N; i.e., isMin s.card.

Русский

Существует градация от натуральных чисел к Finset α так, что если s минимально, то card(s) минимально в ℕ; т.е. isMin s.card.

LaTeX

$$$ \text{isMin}(s) \to \text{isMin}(s.\text{card}) $$$

Lean4

instance instGradeMinOrder_nat : GradeMinOrder ℕ (Finset α)
    where
  grade := card
  grade_strictMono := card_strictMono
  covBy_grade _ _ := CovBy.card_finset
  isMin_grade s hs := by rw [isMin_iff_eq_bot.1 hs]; exact isMin_bot

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