mk_le_iff_forall_finset_subset_card_le

English

For t ⊆ Set α, t.card ≤ n is equivalent to: for all Finset s, s ⊆ t implies s.card ≤ n.

Русский

Для множества t ⊆ α справедливо: t.card ≤ n тогда и только тогда, когда для каждого Finset s верно, что s ⊆ t → s.card ≤ n.

LaTeX

$$$|t| \\le n \\iff \\forall s:\\mathrm{Finset}\\; \\alpha, (s \\subseteq t) \\to s.dcard ≤ n$$$

Lean4

theorem mk_le_iff_forall_finset_subset_card_le {α : Type u} {n : ℕ} {t : Set α} :
    #t ≤ n ↔ ∀ s : Finset α, (s : Set α) ⊆ t → s.card ≤ n :=
  by
  refine ⟨fun H s hs ↦ by simpa using (mk_le_mk_of_subset hs).trans H, fun H ↦ ?_⟩
  apply card_le_of (fun s ↦ ?_)
  classical
  let u : Finset α := s.image Subtype.val
  have : u.card = s.card := Finset.card_image_of_injOn Subtype.coe_injective.injOn
  rw [← this]
  apply H
  simp only [u, Finset.coe_image, image_subset_iff, Subtype.coe_preimage_self, subset_univ]

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