eq_of_subset_of_encard_le' — Mathlib

English

If T is finite and S ⊆ T with T.encard ≤ S.encard, then S = T.

Русский

Если T конечен и S ⊆ T и T.encard ≤ S.encard, тогда S = T.

LaTeX

$$$\operatorname{Finite}(T) \land S \subseteq T \land T.encard \le S.encard \Rightarrow S = T$$$

Lean4

theorem eq_of_subset_of_encard_le' (ht : t.Finite) (hst : s ⊆ t) (hts : t.encard ≤ s.encard) : s = t :=
  by
  rw [← zero_add (a := encard s), ← encard_diff_add_encard_of_subset hst] at hts
  have hdiff := WithTop.le_of_add_le_add_right (ht.subset hst).encard_lt_top.ne hts
  rw [nonpos_iff_eq_zero, encard_eq_zero, diff_eq_empty] at hdiff
  exact hst.antisymm hdiff

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