isGLB_sInf — Mathlib

English

The infimum sInf S is the greatest lower bound of S in the subfield lattice.

Русский

Наименьшее нижнее ограничение sInf S является наибольшим нижним пределом для множества S в решетке подполья.

LaTeX

$$$\text{IsGLB}(S,\, sInf S)$$$

Lean4

theorem isGLB_sInf (S : Set (Subfield K)) : IsGLB S (sInf S) :=
  by
  have : ∀ {s t : Subfield K}, (s : Set K) ≤ t ↔ s ≤ t := by simp [SetLike.coe_subset_coe]
  refine IsGLB.of_image this ?_
  convert isGLB_biInf (s := S) (f := SetLike.coe)
  exact coe_sInf _

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