English
There exists a bottom element in the poset of partial linear maps from E to F (over R); this bottom map has the smallest domain (⊥) and is below every other partial linear map.
Русский
В частичных линейных отображениях от E к F над кольцом R существует наименьший элемент; он имеет минимальную область определения (⊥) и лежит внизу любой другой частичной линейной отображения.
LaTeX
$$$\\exists\\,\\text{bot} \\in \\text{LinearPMap}(R,E,F)\\text{ such that }\\forall f \\in \\text{LinearPMap}(R,E,F), \\ \\text{bot} \\le f$$$
Lean4
instance orderBot : OrderBot (E →ₗ.[R] F) where
bot := ⊥
bot_le
f :=
⟨bot_le, fun x y h => by
have hx : x = 0 := Subtype.eq ((mem_bot R).1 x.2)
have hy : y = 0 := Subtype.eq (h.symm.trans (congr_arg _ hx))
rw [hx, hy, map_zero, map_zero]⟩
