Аналіз I, Розділ 8.5: Упорядковані множини

Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

• Огляд PartialOrder, LinearOrder та WellFoundedLT з деякими API.
• Сильна індукція.
• Лема Цорна.

def Chapter8.PartialOrder.mk {X : Type} [LE X] (hrefl : ∀ (x : X), x ≤ x) (hantisymm : ∀ (x y : X), x ≤ y → y ≤ x → x = y) (htrans : ∀ (x y z : X), x ≤ y → y ≤ z → x ≤ z) : PartialOrder X

Equations

• Chapter8.PartialOrder.mk hrefl hantisymm htrans = { le := fun (x1 x2 : X) => x1 ≤ x2, le_refl := hrefl, le_trans := htrans, lt_iff_le_not_ge := ⋯, le_antisymm := hantisymm }

def Chapter8.IsTotal (X : Type) [PartialOrder X] : Prop

Equations

• Chapter8.IsTotal X = ∀ (x y : X), x ≤ y ∨ y ≤ x

noncomputable def Chapter8.LinearOrder.mk {X : Type} [PartialOrder X] (htotal : IsTotal X) : LinearOrder X

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Chapter8.LinearOrder.subtype {X : Type} [LinearOrder X] (A : Set X) : LinearOrder ↑A

Equations

• Chapter8.LinearOrder.subtype A = Chapter8.LinearOrder.mk ⋯

theorem Chapter8.IsTotal.subtype {X : Type} [PartialOrder X] {A : Set X} (hA : IsTotal X) : IsTotal ↑A

theorem Chapter8.IsTotal.subset {X : Type} [PartialOrder X] {A B : Set X} (hA : IsTotal ↑A) (hAB : B ⊆ A) : IsTotal ↑B

@[reducible, inline]

abbrev Chapter8.X_8_5_4 : Set (Set ℕ)

Equations

• Chapter8.X_8_5_4 = {{1, 2}, {2}, {2, 3}, {2, 3, 4}, {5}}

theorem Chapter8.IsMax.iff {X : Type} [PartialOrder X] (x : X) : IsMax x ↔ ¬∃ (y : X), x < y

Визначення 8.5.5 (Maximal and minimal elements). Here we use Mathlib's IsMax and IsMin.

theorem Chapter8.IsMin.iff {X : Type} [PartialOrder X] (x : X) : IsMin x ↔ ¬∃ (y : X), x > y

theorem Chapter8.WellFoundedLT.iff (X : Type) [LinearOrder X] : WellFoundedLT X ↔ ∀ (A : Set X), A.Nonempty → ∃ (x : ↑A), IsMin x

Визначення 8.5.8. Ми використовуємо [LinearOrder X] [WellFoundedLT X] для опису добре впорядкованих множин.

theorem Chapter8.WellFoundedLT.iff' {X : Type} [PartialOrder X] (h : IsTotal X) : WellFoundedLT X ↔ ∀ (A : Set X), A.Nonempty → ∃ (x : ↑A), IsMin x

theorem Chapter8.IsMax.ofFinite {X : Type} [LinearOrder X] [Finite X] [Nonempty X] : ∃ (x : X), IsMax x

Вправа 8.5.8

theorem Chapter8.IsMin.ofFinite {X : Type} [LinearOrder X] [Finite X] [Nonempty X] : ∃ (x : X), IsMin x

theorem Chapter8.WellFoundedLT.ofFinite {X : Type} [LinearOrder X] [Finite X] : WellFoundedLT X

Вправа 8.5.8

theorem Chapter8.WellFoundedLT.subset {X : Type} [PartialOrder X] {A B : Set X} (hA : IsTotal ↑A) [hwell : WellFoundedLT ↑A] (hAB : B ⊆ A) : WellFoundedLT ↑B

theorem Chapter8.WellFoundedLT.strong_induction {X : Type} [LinearOrder X] [WellFoundedLT X] {P : X → Prop} (h : ∀ (n : X), (∀ m < n, P m) → P n) (n : X) : P n

Твердження 8.5.10 / Вправа 8.5.10

@[reducible, inline]

abbrev Chapter8.IsUpperBound {X : Type} [PartialOrder X] (A : Set X) (x : X) : Prop

Визначення 8.5.12 (Верхні межі та точні верхні межі)

Equations

• Chapter8.IsUpperBound A x = ∀ y ∈ A, y ≤ x

theorem Chapter8.IsUpperBound.iff {X : Type} [PartialOrder X] (A : Set X) (x : X) : IsUpperBound A x ↔ x ∈ upperBounds A

Зв'язок із Mathlib-овським upperBounds

@[reducible, inline]

abbrev Chapter8.IsStrictUpperBound {X : Type} [PartialOrder X] (A : Set X) (x : X) : Prop

Equations

• Chapter8.IsStrictUpperBound A x = (Chapter8.IsUpperBound A x ∧ x ∉ A)

theorem Chapter8.IsStrictUpperBound.iff {X : Type} [PartialOrder X] (A : Set X) (x : X) : IsStrictUpperBound A x ↔ ∀ y ∈ A, y < x

theorem Chapter8.IsStrictUpperBound.iff' {X : Type} [PartialOrder X] (A : Set X) (x : X) : IsStrictUpperBound A x ↔ x ∈ upperBounds A \ A

theorem Chapter8.IsMin.iff_lowerbound {X : Type} [PartialOrder X] {Y : Set X} (hY : IsTotal ↑Y) (x₀ : X) : (∃ (hx₀ : x₀ ∈ Y), IsMin ⟨x₀, hx₀⟩) ↔ x₀ ∈ Y ∧ ∀ x ∈ Y, x₀ ≤ x

Зручний спосіб спростити поняття наявності x₀ як мінімального елемента.

theorem Chapter8.IsMin.iff_lowerbound' {X : Type} [PartialOrder X] {Y : Set X} (hY : IsTotal ↑Y) : (∃ (x₀ : ↑Y), IsMin x₀) ↔ ∃ x₀ ∈ Y, ∀ x ∈ Y, x₀ ≤ x

theorem Chapter8.WellFoundedLT.partialOrder {X : Type} [PartialOrder X] (x₀ : X) : ∃ (Y : Set X), IsTotal ↑Y ∧ WellFoundedLT ↑Y ∧ (∃ (hx₀ : x₀ ∈ Y), IsMin ⟨x₀, hx₀⟩) ∧ ¬∃ (x : X), IsStrictUpperBound Y x

Лема 8.5.14

theorem Chapter8.Zorns_lemma {X : Type} [PartialOrder X] [Nonempty X] (hchain : ∀ (Y : Set X), IsTotal ↑Y ∧ Y.Nonempty → ∃ (x : X), IsUpperBound Y x) : ∃ (x : X), IsMax x

Лема 8.5.15 (Лема Цорна) / Вправа 8.5.14

def Chapter8.empty_set_partial_order [h₀ : LE Empty] : Decidable (∃ (h : PartialOrder Empty), LE.le = LE.le)

Вправа 8.5.1

Equations

• Chapter8.empty_set_partial_order = sorry

def Chapter8.empty_set_linear_order [h₀ : LE Empty] : Decidable (∃ (h : LinearOrder Empty), LE.le = LE.le)

Equations

• Chapter8.empty_set_linear_order = sorry

def Chapter8.empty_set_well_order [h₀ : LT Empty] : Decidable (Nonempty (WellFoundedLT Empty))

Equations

• Chapter8.empty_set_well_order = sorry

def Chapter8.Ex_8_5_5_b : Decidable (∀ (X Y : Type) (h : LinearOrder Y) (f : X → Y), ∃ (h₀ : LinearOrder X), LE.le = fun (x y : X) => f x < f y ∨ x = y)

Equations

• Chapter8.Ex_8_5_5_b = sorry

@[reducible, inline]

abbrev Chapter8.OrderIdeals (X : Type) [PartialOrder X] : Set (Set X)

Вправа 8.5.6

Equations

• Chapter8.OrderIdeals X = Set.Iic '' Set.univ

def Chapter8.OrderIdeals.iso {X : Type} [PartialOrder X] : X ≃o ↑(OrderIdeals X)

Equations

• Chapter8.OrderIdeals.iso = { toFun := fun (x : X) => ⟨Set.Iic x, ⋯⟩, invFun := sorry, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

def Chapter8.Lex' (α : Type) : Type

Вправа 8.5.12. Тут ми робимо копію обгортки Lex з Mathlib для лексикографічних упорядкувань. -- Ця обгортка потрібна, оскільки добутки X × Y упорядкованих множин за замовчуванням -- отримують інстанцію добуткового часткового порядку, а не лексикографічного.

Equations

• Chapter8.Lex' α = α

instance Chapter8.Lex'.partialOrder {X Y : Type} [PartialOrder X] [PartialOrder Y] : PartialOrder (Lex' (X × Y))

Equations

• One or more equations did not get rendered due to their size.

instance Chapter8.Lex'.linearOrder {X Y : Type} [LinearOrder X] [LinearOrder Y] : LinearOrder (Lex' (X × Y))

Equations

• Chapter8.Lex'.linearOrder = sorry

instance Chapter8.Lex'.WellFoundedLT {X Y : Type} [LinearOrder X] [_root_.WellFoundedLT X] [LinearOrder Y] [_root_.WellFoundedLT Y] : _root_.WellFoundedLT (Lex' (X × Y))