map_inr — Mathlib

English

If f is a MonoidEquiv, then x ∈ K.map f ↔ f.symm x ∈ K for K ⊆ M.

Русский

Если f — эквив моноидов, то x ∈ K.map f ↔ f.symm x ∈ K.

LaTeX

$$$ x \in K.map f \iff f^{-1}(x) \in K. $$$

Lean4

@[to_additive]
theorem map_inr (s : Submonoid N) : s.map (inr M N) = prod ⊥ s :=
  ext fun p =>
    ⟨fun ⟨_, hx, hp⟩ => hp ▸ ⟨Set.mem_singleton 1, hx⟩, fun ⟨hp1, hps⟩ =>
      ⟨p.2, hps, Prod.ext (Set.eq_of_mem_singleton hp1).symm rfl⟩⟩

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