English
A substantive construction proving one of the HImp axioms for nuclei.
Русский
Существенная конструкция доказательства одного из аксиом импликации HImp для нуклеусов.
LaTeX
$$$\text{HImp}$ axioms hold in $Nucleus(X)$$$
Lean4
instance : HImp (Nucleus X) where
himp m
n :=
{ toFun x := ⨅ y ≥ x, m y ⇨ n y
idempotent'
x :=
le_iInf₂ fun y hy ↦
calc
⨅ z ≥ ⨅ w ≥ x, m w ⇨ n w, m z ⇨ n z
_ ≤ m (m y ⇨ n y) ⇨ n (m y ⇨ n y) := (iInf₂_le _ <| biInf_le _ hy)
_ = m y ⇨ n y := by rw [map_himp_apply, himp_himp, ← map_inf, inf_of_le_right (le_trans n.le_apply le_himp)]
map_inf' x
y := by
simp only [and_assoc, le_antisymm_iff, le_inf_iff, le_iInf_iff]
refine ⟨fun z hxz ↦ iInf₂_le _ <| inf_le_of_left_le hxz, fun z hyz ↦ iInf₂_le _ <| inf_le_of_right_le hyz, ?_⟩
have : Nonempty X := ⟨x⟩
simp only [iInf_inf, le_iInf_iff, le_himp_iff, iInf_le_iff, le_inf_iff, forall_and, forall_const, and_imp]
intro k hxyk l hlx hly hlk
calc
l = (l ⊓ m (x ⊔ k)) ⊓ (l ⊓ m (y ⊔ k)) := by
rw [← inf_inf_distrib_left, ← map_inf, ← sup_inf_right, sup_eq_right.2 hxyk, inf_eq_left.2 hlk]
_ ≤ n (x ⊔ k) ⊓ n (y ⊔ k) := by gcongr; exacts [hlx (x ⊔ k) le_sup_left, hly (y ⊔ k) le_sup_left]
_ = n k := by rw [← map_inf, ← sup_inf_right, sup_eq_right.2 hxyk]
le_apply' := by simpa using fun _ _ h ↦ inf_le_of_left_le <| h.trans n.le_apply }
