ofHoms_homFamily — Mathlib

English

For any P, transporting the homomorphism family via homFamily recovers P: ofHoms P.homFamily = P.

Русский

Для любого P перенос семейства гомоморфизмов через homFamily восстанавливает P: ofHoms P.homFamily = P.

LaTeX

$$$\mathrm{ofHoms}(\mathrm{homFamily}) = P$$$

Lean4

@[simp]
theorem ofHoms_homFamily (P : MorphismProperty C) : ofHoms P.homFamily = P :=
  by
  ext _ _ f
  constructor
  · intro hf
    rw [ofHoms_iff] at hf
    obtain ⟨⟨f, hf⟩, ⟨_, _⟩⟩ := hf
    exact hf
  · intro hf
    exact ⟨(⟨f, hf⟩ : P.toSet)⟩

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