symm_iff — Mathlib

English

The image property is symmetric with respect to taking inverses: IsImage(e, s, t) holds iff IsImage(e^{-1}, t, s) holds.

Русский

Свойство образа симметрично по отношению к взятию обратного отображения: IsImage(e, s, t) эквивалентно IsImage(e^{-1}, t, s).

LaTeX

$$$IsImage(e^{-1}, t, s) \\iff IsImage(e, s, t)$$$

Lean4

@[simp]
theorem symm_iff : e.symm.IsImage t s ↔ e.IsImage s t :=
  ⟨fun h => h.symm, fun h => h.symm⟩

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