mker_snd — Mathlib

English

Let snd be the projection onto the second coordinate from M × N to N. Its kernel is the submonoid ⊤ × ⊥, i.e. all pairs (m, 1_N).

Русский

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

LaTeX

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

Lean4

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

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