symm_apply_mem_iff_mem_image — Mathlib

English

For an equivalence e: α ≃ β and a set s ⊆ α, membership of e.symm x in s is equivalent to x belonging to the image of s under e.

Русский

Для эквиваленции e: α ≃ β и множества s ⊆ α члены e.symm x ∈ s эквивалентны тому, что x принадлежит образу s под e.

LaTeX

$$e.symm x ∈ s \iff x ∈ e '' s$$

Lean4

theorem symm_apply_mem_iff_mem_image {α β : Type*} (e : α ≃ β) (s : Set α) (x : β) : e.symm x ∈ s ↔ x ∈ e '' s :=
  ⟨fun h => ⟨e.symm x, h, by simp⟩, by
    rintro ⟨a, m, rfl⟩
    simpa using m⟩

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