English
The dual structure of filters is captured by the statement that Filter α satisfies a minimal set of axioms making it a Coframe. In particular, the dual of the lattice operations behaves according to the infimum-supremum interplay.
Русский
Двойственная структура фильтров описывается тем, что Filter α удовлетворяет минимальному набору аксиом, превращая его в кофрейм. В частности, двойственная связь между операциями Inf и Sup выполняется согласно взаимодействию infimum и supremum.
LaTeX
$$$ \text{Coframe.MinimalAxioms} (\mathrm{Filter}\; \alpha) \text{ holds with } iInf\_sup\_le\_sup\_sInf, \dots $$$
Lean4
/-- The dual version does not hold! `Filter α` is not a `CompleteDistribLattice`. -/
-- See note [reducible non-instances]
abbrev coframeMinimalAxioms : Coframe.MinimalAxioms (Filter α) :=
{ Filter.instCompleteLatticeFilter with
iInf_sup_le_sup_sInf := fun f s t ⟨h₁, h₂⟩ => by
classical
rw [iInf_subtype']
rw [sInf_eq_iInf', ← Filter.mem_sets, iInf_sets_eq_finite, mem_iUnion] at h₂
obtain ⟨u, hu⟩ := h₂
rw [← Finset.inf_eq_iInf] at hu
suffices ⨅ i : s, f ⊔ ↑i ≤ f ⊔ u.inf fun i => ↑i from this ⟨h₁, hu⟩
refine Finset.induction_on u (le_sup_of_le_right le_top) ?_
rintro ⟨i⟩ u _ ih
rw [Finset.inf_insert, sup_inf_left]
exact le_inf (iInf_le _ _) ih }
