subset_symm_image — Mathlib

English

For any bijection e and sets s,t, s ⊆ e⁻¹''t iff e''s ⊆ t.

Русский

Для биекции e и множеств s,t верно: s ⊆ e⁻¹''t эквивалентно e''s ⊆ t.

LaTeX

$$$s \subseteq e^{-1}''t \;\Longleftrightarrow\; e''s \subseteq t.$$$

Lean4

@[simp high]
protected theorem subset_symm_image {α β} (e : α ≃ β) (s : Set α) (t : Set β) : s ⊆ e.symm '' t ↔ e '' s ⊆ t :=
  calc
    s ⊆ e.symm '' t ↔ e.symm.symm '' s ⊆ t := by rw [e.symm.symm_image_subset]
    _ ↔ e '' s ⊆ t := by rw [e.symm_symm]

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