comp — Mathlib

English

If hf' is Semiconj₂ f' gb gc and hf is Semiconj₂ f ga gb, then Semiconj₂ (f' ∘ f) ga gc.

Русский

Если hf' — Semiconj₂ f' gb gc и hf — Semiconj₂ f ga gb, то Semiconj₂ (f' ∘ f) ga gc.

LaTeX

$$$ \text{Semiconj₂}(f' \circ f, ga, gc) $$$

Lean4

theorem comp {f' : β → γ} {gc : γ → γ → γ} (hf' : Semiconj₂ f' gb gc) (hf : Semiconj₂ f ga gb) :
    Semiconj₂ (f' ∘ f) ga gc := fun x y ↦ by simp only [hf'.eq, hf.eq, comp_apply]

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