English
For any a, s: Finset α, t: Finset α, a ∈ s, we have a basic truth about membership in the difference s \ t.
Русский
Для любого a, s, t верно свойство членства в разности s \ t.
LaTeX
$$$a \in s \setminus t \iff a \in s \land a \notin t$$$
Lean4
/-- Initial segments are nested in some way. In particular, if they're the same size they're equal.
-/
theorem total (h₁ : IsInitSeg 𝒜₁ r) (h₂ : IsInitSeg 𝒜₂ r) : 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁ := by
classical
simp_rw [← sdiff_eq_empty_iff_subset, ← not_nonempty_iff_eq_empty]
by_contra! h
have ⟨⟨s, hs⟩, t, ht⟩ := h
rw [mem_sdiff] at hs ht
obtain hst | hst | hts := trichotomous_of (α := Colex (Finset α)) (· < ·) (toColex s) (toColex t)
· exact hs.2 <| h₂.2 ht.1 ⟨hst, h₁.1 hs.1⟩
· simp only [toColex_inj] at hst
exact ht.2 <| hst ▸ hs.1
· exact ht.2 <| h₁.2 hs.1 ⟨hts, h₂.1 ht.1⟩
