gi — Mathlib · SciLib

English

Closure and inclusion form a Galois insertion between Set(K) and Subfield(K).

Русский

Замыкание и включение образуют вставку Галоиса между множеством(K) и подпольем(K).

LaTeX

$$$\text{closure} \dashv \text{incl}$$$

Lean4

/-- `closure` forms a Galois insertion with the coercion to set. -/
protected def gi : GaloisInsertion (@closure K _) (↑)
    where
  choice s _ := closure s
  gc _ _ := closure_le
  le_l_u _ := subset_closure
  choice_eq _ _ := rfl

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