comp_fst — Mathlib

English

If f is Theta in the first argument after projecting to the first coordinate, then the composition with fst preserves Theta.

Русский

Если Θ сохраняется при проекции на первую координату, то композиция с fst сохраняет Θ.

LaTeX

$$$\forall f,g:\; f =Θ[l] g \Rightarrow (f \circ \mathrm{Prod}.fst) =Θ[l\times^s l'] (g \circ \mathrm{Prod}.fst)$$$

Lean4

protected theorem comp_fst : f =Θ[l] g → (f ∘ Prod.fst) =Θ[l ×ˢ l'] (g ∘ Prod.fst) :=
  by
  simp only [IsTheta]
  exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.comp_fst l', h₂.comp_fst l'⟩

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