English
For a subset S of T, kernel(S) is defined as the infimum in α of the image of S under the inclusion map from T to α; that is, kernel(S) = sInf { val(x) : x ∈ S }.
Русский
Для подмножества S ⊆ T kernel(S) задаётся как наименьшая нижняя граница элементов S в α: kernel(S) = sInf {val(x) : x ∈ S}.
LaTeX
$$$\\text{kernel}(S) := \\sInf(\\mathrm{val}''S).$$$
Lean4
/-- For a subset `S` of `T`, `kernel S` is the infimum of `S` (considered as a set of `α`) -/
abbrev kernel (S : Set T) :=
sInf
(Subtype.val '' S)
/- The pair of maps `kernel` and `hull` form an antitone Galois connection between the
subsets of `T` and `α`. -/