English
There is a LocallyFiniteOrder structure on Finset α, with an explicit description of Icc via differences and powersets, and with a compatible le relation defined by subset inclusion; the Icc and related intervals are described by finite constructions using s, t, u and powerset notions.
Русский
Простая локально конечная упорядоченность на Finset α: Icc между двумя конечными множествами описывается через разности и множества подмножеств, совместимая отношение — включение подмножеств; интервалы задаются конечными конструкциями через множества подмножеств.
LaTeX
$$$\\text{instLocallyFiniteOrder} : \\text{LocallyFiniteOrder}(\\operatorname{Finset} \\ α).$$$
Lean4
/-- `LocallyFiniteOrder` instance for `Finset α`.
We provide an optimized definition for `Finset.Icc (s : Finset α) t`,
then define the other intervals based on `Icc`.
We do not define, e.g., `Finset.Ico` based on `Finset.ssubsets`,
because it would require more code without performance gain.
-/
instance instLocallyFiniteOrder [DecidableEq α] : LocallyFiniteOrder (Finset α) :=
.ofIcc _
(fun s t ↦
if s ⊆ t then
(t \ s).powerset.attach.map
⟨fun u ↦ u.1.disjUnion s <| disjoint_sdiff_self_left.mono_left <| mem_powerset.mp u.2, fun u₁ u₂ h ↦ by
simpa only [disjUnion_inj_left, Subtype.eq_iff] using h⟩
else ∅)
fun s t u ↦ by
by_cases hst : s ⊆ t
· suffices (∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u) ↔ s ⊆ u ∧ u ⊆ t by simpa [hst, subset_sdiff, and_assoc]
constructor
· rintro ⟨u, hut, -, rfl⟩
exact ⟨subset_union_right, union_subset hut hst⟩
· rintro ⟨hsu, hut⟩
exact ⟨u \ s, sdiff_subset.trans hut, disjoint_sdiff_self_left, sdiff_union_of_subset hsu⟩
· suffices s ⊆ u → ¬u ⊆ t by simpa [hst]
exact fun hsu hut ↦ hst (hsu.trans hut)
