symm_image_subset — Mathlib

English

For any bijection e and set S, Set.image e S = Set.preimage e.symm S.

Русский

Для биекции e и множества S верно: Set.image e S = Set.preimage e.symm S.

LaTeX

$$$\operatorname{image}(e) S = \operatorname{preimage}(e^{-1}) S.$$$

Lean4

@[simp high]
protected theorem symm_image_subset {α β} (e : α ≃ β) (s : Set α) (t : Set β) : e.symm '' t ⊆ s ↔ t ⊆ e '' s := by
  rw [image_subset_iff, e.image_eq_preimage]
    -- Increased priority so this fires before `image_subset_iff`

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