eq_of_subset_of_card_le — Mathlib

English

If s ⊆ t and |t| ≤ |s| then s = t (alternative formulation).

Русский

Если s ⊆ t и |t| ≤ |s|, тогда s = t (альтернативная формулировка).

LaTeX

$$$ hsub : s \\subseteq t \\rightarrow hcard : |t| \\le |s| \\rightarrow s = t $$$

Lean4

theorem eq_of_subset_of_card_le {s t : Set α} [Fintype s] [Fintype t] (hsub : s ⊆ t)
    (hcard : Fintype.card t ≤ Fintype.card s) : s = t :=
  (eq_or_ssubset_of_subset hsub).elim id fun h => absurd hcard <| not_le_of_gt <| card_lt_card h

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