mem_map_equiv — Mathlib

English

For a subsemigroup K of M and an equivalence f: M ≃* N, membership in K.map f corresponds to membership in K of the preimage under f.symm.

Русский

Для K ⊆ M и эквивалентности f: M ≃* N членство в K.map f эквивалентно членству в K в предобразе f.symm.

LaTeX

$$$x \\in K.map f ↔ f^{-1}(x) ∈ K$ for f an equivalence$$

Lean4

@[to_additive]
theorem mem_map_equiv {f : M ≃* N} {K : Subsemigroup M} {x : N} : x ∈ K.map (f : M →ₙ* N) ↔ f.symm x ∈ K :=
  @Set.mem_image_equiv _ _ (K : Set M) f.toEquiv x

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