symmetrify — Mathlib

English

If φ is a covering prefunctor, then its symmetrification φ.symmetrify is also a covering prefunctor.

Русский

Если φ — покрывающий префунктор, то его симметризация φ.symmetrify тоже является покрывающим префунктором.

LaTeX

$$\operatorname{IsCovering}(\phi) \Rightarrow \operatorname{IsCovering}(\phi.\mathrm{symmetrify})$$

Lean4

protected theorem symmetrify (hφ : φ.IsCovering) : φ.symmetrify.IsCovering := by
  refine ⟨fun u => ?_, fun u => ?_⟩ <;>
    simp [φ.symmetrifyStar, φ.symmetrifyCostar, hφ.star_bijective u, hφ.costar_bijective u]

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