English
Defines Infimum set structure on the class of nuclei in a complete lattice setting.
Русский
Определяет структуру инфимума множества над классом нуклеусов в полном решении.
LaTeX
$$$\text{InfSet}(Nucleus(X))$$$
Lean4
instance : InfSet (Nucleus X) where
sInf
s :=
{ toFun x := ⨅ f ∈ s, f x,
map_inf' x
y := by
simp only [InfHomClass.map_inf, le_antisymm_iff, le_inf_iff, le_iInf_iff]
refine ⟨⟨?_, ?_⟩, ?_⟩ <;> rintro f hf
· exact iInf₂_le_of_le f hf inf_le_left
· exact iInf₂_le_of_le f hf inf_le_right
· exact ⟨inf_le_of_left_le <| iInf₂_le f hf, inf_le_of_right_le <| iInf₂_le f hf⟩
idempotent' x := iInf₂_mono fun f hf ↦ (f.monotone <| iInf₂_le f hf).trans_eq (f.idempotent _)
le_apply' x := by simp [le_apply] }
