mker_fst — Mathlib

English

Let fst be the projection onto the first coordinate from M × N to M. Its kernel is the submonoid ⊥ × ⊤, i.e. all pairs (1_M, n).

Русский

Пусть fst — проекция из M × N на M. Её ядро равно ⊥ × ⊤, то есть все пары (1_M, n).

LaTeX

$$$ \operatorname{mker}(\operatorname{fst} M N) = \mathrm{prod} \bot \top $$$

Lean4

@[to_additive (attr := simp)]
theorem mker_fst : mker (fst M N) = .prod ⊥ ⊤ :=
  SetLike.ext fun _ => (iff_of_eq (and_true _)).symm

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