normalizedFactorsEquivOfQuotEquiv_symm

English

The bijection between the sets of normalized factors preserves the underlying sets via a quotient equivalence.

Русский

Биекция между множествами нормализованных факторов сохраняет исходные множества через эквивалентность квоти.

LaTeX

$$normalizedFactorsEquivOfQuotEquiv$$

Lean4

@[simp]
theorem normalizedFactorsEquivOfQuotEquiv_symm (hI : I ≠ ⊥) (hJ : J ≠ ⊥) :
    (normalizedFactorsEquivOfQuotEquiv f hI hJ).symm = normalizedFactorsEquivOfQuotEquiv f.symm hJ hI :=
  rfl

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