whiskerLeft_iff — Mathlib

English

Left whiskering by the identity on the left is injective on 2-cells: 𝟙 a ◁ η = 𝟙 a ◁ θ iff η = θ.

Русский

Левое висение на 𝟙 a инъективно на 2-ячейках: 𝟙 a ◁ η = 𝟙 a ◁ θ тогда и только тогда η = θ.

LaTeX

$$$ 𝟙_a \\triangleleft η = 𝟙_a \\triangleleft θ \\; \\Longleftrightarrow \\; η = θ $$$

Lean4

theorem whiskerLeft_iff {f g : a ⟶ b} (η θ : f ⟶ g) : 𝟙 a ◁ η = 𝟙 a ◁ θ ↔ η = θ := by simp

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