kernel — Mathlib

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 `α`. -/

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