subset_map_symm — Mathlib

English

The Finset version of Equiv.symm_image_subset: t.map f.symm ⊆ s ↔ t ⊆ s.map f.

Русский

Версия Finset для Equiv.symm_image_subset: t.map f.symm ⊆ s ⇔ t ⊆ s.map f.

LaTeX

$$$t.map f.symm \subseteq s \iff t \subseteq s.map f$$$

Lean4

/-- The `Finset` version of `Equiv.subset_symm_image`. -/
theorem subset_map_symm {t : Finset β} {f : α ≃ β} : s ⊆ t.map f.symm ↔ s.map f ⊆ t :=
  by
  constructor <;> intro h x hx
  · simp only [mem_map_equiv] at hx
    simpa using h hx
  · simp only [mem_map_equiv]
    exact h (by simp [hx])

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