sectL — Mathlib

English

Fixing an element b ∈ β gives an embedding α ↪ α × β, a ↦ (a,b).

Русский

Фиксируя элемент b ∈ β, получаем вложение α ↪ α × β, a ↦ (a,b).

LaTeX

$$$\\mathrm{sectL}(\\alpha,\\beta)(b): \\alpha \\hookrightarrow \\alpha \\times \\beta,\\; a \\mapsto (a,b)$$$

Lean4

/-- Fixing an element `b : β` gives an embedding `α ↪ α × β`. -/
@[simps]
def sectL (α : Sort _) {β : Sort _} (b : β) : α ↪ α × β :=
  ⟨fun a => (a, b), fun _ _ h => congr_arg Prod.fst h⟩

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