lift'_fst — Mathlib

English

For a representable F with f' and a morphism g, F.map (hf'.fst' g) ≈ hf'.fst g after fullness.

Русский

Для представляемого F и f' и морфизма g выполняется приблизительное равенство между F.map и hf'.fst.

LaTeX

$$$$ F.map (hf'.fst' g) = hf'.fst g $$$$

Lean4

@[reassoc (attr := simp)]
theorem lift'_fst [Full F] [Faithful F] : hf'.lift' i h hi ≫ hf'.fst' g = i :=
  F.map_injective (by simp [lift'])

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