giLowerClosureCoe — Mathlib

English

The lower closure operator forms a Galois insertion with the coercion to sets.

Русский

Оператор нижнего замыкания образует вставку Галуа с приводом к множествам.

LaTeX

$${α : Type u} → [Preorder α] → GaloisInsertion (lowerClosure : Set α → LowerSet α) (↑)$$

Lean4

/-- `lowerClosure` forms a Galois insertion with the coercion from lower sets to sets. -/
def giLowerClosureCoe : GaloisInsertion (lowerClosure : Set α → LowerSet α) (↑)
    where
  choice s hs := ⟨s, fun a _b hba ha => hs ⟨a, ha, hba⟩⟩
  gc := gc_lowerClosure_coe
  le_l_u _ := subset_lowerClosure
  choice_eq _s hs := SetLike.coe_injective <| subset_lowerClosure.antisymm hs

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