equiv_image_eq_iff_subset — Mathlib

English

Let e be a bijection e: α ≃ α and s a finite subset of α. Then e[s] = s if and only if e[s] ⊆ s.

Русский

Пусть e — биекция α → α и s — конечное подмножество α. Тогда e(s) = s тогда и только тогда, когда e(s) ⊆ s.

LaTeX

$$$\\\\forall \\, \\alpha \\,\\\\forall \\, s \subseteq \\alpha \\,\\\\forall \\, e:\\\\alpha \\\\simeq \\\\alpha, \\\\\\u200b Finite(s) \\\\Rightarrow \\\\big(e[s] = s \\\\iff e[s] \\subseteq s\\\\).$$$

Lean4

theorem equiv_image_eq_iff_subset (e : α ≃ α) (hs : s.Finite) : e '' s = s ↔ e '' s ⊆ s :=
  ⟨fun h ↦ by rw [h], fun h ↦ hs.eq_of_subset_of_card_le h <| ge_of_eq (Nat.card_congr (e.image s).symm)⟩

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