eq_image_iff_symm_image_eq — Mathlib

English

For a measurable equivalence e and sets s ⊆ β, t ⊆ α, we have s = e''t iff e.symm''s = t.

Русский

Для измеримой эквивалентности e и множеств s ⊆ β, t ⊆ α верно: s = e''t ⇔ e.symm''s = t.

LaTeX

$$$ s = e'' t \iff e.symm'' s = t $$$

Lean4

theorem eq_image_iff_symm_image_eq (e : α ≃ᵐ β) (s : Set β) (t : Set α) : s = e '' t ↔ e.symm '' s = t := by
  rw [← coe_toEquiv, Equiv.eq_image_iff_symm_image_eq, coe_toEquiv_symm]

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