mem_map_equiv — Mathlib

English

If f is an equivalence α ≃ β, then b ∈ s.map f.toEmbedding iff f.symm(b) ∈ s.

Русский

Если f — эквивиалент ∼ α ≃ β, то b ∈ s.map f.toEmbedding тогда и только тогда, когда f.symm(b) ∈ s.

LaTeX

$$$ b \in s.map f.toEmbedding \iff f.symm b \in s $$$

Lean4

@[simp 1100]
theorem mem_map_equiv {f : α ≃ β} {b : β} : b ∈ s.map f.toEmbedding ↔ f.symm b ∈ s :=
  by
  rw [mem_map]
  exact
    ⟨by
      rintro ⟨a, H, rfl⟩
      simpa, fun h => ⟨_, h, by simp⟩⟩

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