instOrderBotFinset — Mathlib

English

For any finpartition P of s, the number of blocks is at most the number of elements of s: |P.parts| ≤ |s|.

Русский

Для любого конечного разбиения P множества s число блоков не превосходит |s|.

LaTeX

$$$|P.components| \\le |s|$$$

Lean4

instance (s : Finset α) : OrderBot (Finpartition s) :=
  { (inferInstance : Bot (Finpartition s)) with
    bot_le := fun P t ht ↦ by
      rw [mem_bot_iff] at ht
      obtain ⟨a, ha, rfl⟩ := ht
      obtain ⟨t, ht, hat⟩ := P.exists_mem ha
      exact ⟨t, ht, singleton_subset_iff.2 hat⟩ }

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