Lean4
/-- Sieves on an object `X` form a complete lattice.
We generate this directly rather than using the Galois insertion for nicer definitional properties.
-/
instance : CompleteLattice (Sieve X) where
le S R := ∀ ⦃Y⦄ (f : Y ⟶ X), S f → R f
le_refl _ _ _ := id
le_trans _ _ _ S₁₂ S₂₃ _ _ h := S₂₃ _ (S₁₂ _ h)
le_antisymm _ _ p q := Sieve.ext fun _ _ => ⟨p _, q _⟩
top :=
{ arrows := fun _ => Set.univ
downward_closed := fun _ _ => ⟨⟩ }
bot :=
{ arrows := fun _ => ∅
downward_closed := False.elim }
sup := Sieve.union
inf := Sieve.inter
sSup := Sieve.sup
sInf := Sieve.inf
le_sSup _ S hS _ _ hf := ⟨S, hS, hf⟩
sSup_le := fun _ _ ha _ _ ⟨b, hb, hf⟩ => (ha b hb) _ hf
sInf_le _ _ hS _ _ h := h _ hS
le_sInf _ _ hS _ _ hf _ hR := hS _ hR _ hf
le_sup_left _ _ _ _ := Or.inl
le_sup_right _ _ _ _ := Or.inr
sup_le _ _ _ h₁ h₂ _
f := by --ℰ S hS Y f := by
rintro (hf | hf)
· exact h₁ _ hf
· exact h₂ _ hf
inf_le_left _ _ _ _ := And.left
inf_le_right _ _ _ _ := And.right
le_inf _ _ _ p q _ _ z := ⟨p _ z, q _ z⟩
le_top _ _ _ _ := trivial
bot_le _ _ _ := False.elim
