symm_apply_mem_iff — Mathlib

English

If e.IsImage s t, then for every y in the target of e, the inverse image under e of y lies in s exactly when y lies in t.

Русский

Если e.IsImage s t, то для каждого y из целого множества e, обратное изображение e(y) принадлежит s тогда и только тогда y принадлежит t.

LaTeX

$$IsImage(e, s, t) \\Rightarrow \\forall y \\in e.target, e^{-1}(y) \\in s \\iff y \\in t$$

Lean4

theorem symm_apply_mem_iff (h : e.IsImage s t) (hy : y ∈ e.target) : e.symm y ∈ s ↔ y ∈ t :=
  h.symm hy

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