Maximal length of chains

This file contains lemmas to work with the maximal lengths of chains of arbitrary relations. See Order.height for a definition specialized to finding the height of an element in a preorder.

Main definition

• Set.chainHeight: The maximal length of a chain in a set s with relation r.

Main results

• Set.exists_isChain_of_le_chainHeight: For each n : ℕ such that n ≤ s.chainHeight, there exists a subset t of length n such that IsChain r t.
• Set.chainHeight_mono: If s ⊆ t then s.chainHeight ≤ t.chainHeight.
• Set.chainHeight_eq_of_relEmbedding: If f is an relation embedding, then (f '' s).chainHeight = s.chainHeight.

noncomputable def Set.chainHeight {α : Type u_1} (s : Set α) (r : α → α → Prop) : ℕ∞

The maximal length of a chain in a set s with relation r.

Equations

• s.chainHeight r = ⨆ (t : { t : Set α // t ⊆ s ∧ IsChain r t }), (↑t).encard

theorem Set.chainHeight_eq_iSup {α : Type u_1} (s : Set α) (r : α → α → Prop) : s.chainHeight r = ⨆ (t : { t : Set α // t ⊆ s ∧ IsChain r t }), (↑t).encard

theorem Set.chainHeight_le_encard {α : Type u_1} (s : Set α) (r : α → α → Prop) : s.chainHeight r ≤ s.encard

theorem Set.chainHeight_ne_top_of_finite {α : Type u_1} (s : Set α) (r : α → α → Prop) (h : s.Finite) : s.chainHeight r ≠ ⊤

theorem Set.exists_isChain_of_le_chainHeight {α : Type u_1} {r : α → α → Prop} {s : Set α} (n : ℕ) (h : ↑n ≤ s.chainHeight r) : ∃ t ⊆ s, t.encard = ↑n ∧ IsChain r t

theorem Set.exists_eq_chainHeight_of_chainHeight_ne_top {α : Type u_1} (s : Set α) (r : α → α → Prop) (h : s.chainHeight r ≠ ⊤) : ∃ t ⊆ s, t.encard = s.chainHeight r ∧ IsChain r t

theorem Set.exists_eq_chainHeight_of_finite {α : Type u_1} (s : Set α) (r : α → α → Prop) (h : s.Finite) : ∃ t ⊆ s, t.encard = s.chainHeight r ∧ IsChain r t

theorem Set.encard_le_chainHeight_of_isChain {α : Type u_1} {r : α → α → Prop} (s t : Set α) (hs : t ⊆ s) (hc : IsChain r t) : t.encard ≤ s.chainHeight r

theorem Set.encard_eq_chainHeight_of_isChain {α : Type u_1} {r : α → α → Prop} (s : Set α) (hc : IsChain r s) : s.encard = s.chainHeight r

theorem Set.finite_of_chainHeight_ne_top {α : Type u_1} {r : α → α → Prop} {s : Set α} (hc : IsChain r s) (h : s.chainHeight r ≠ ⊤) : s.Finite

theorem Set.not_isChain_of_chainHeight_lt_encard {α : Type u_1} (r : α → α → Prop) (s t : Set α) (ht : t ⊆ s) (he : s.chainHeight r < t.encard) : ¬IsChain r t

theorem Set.chainHeight_eq_top_iff {α : Type u_1} (s : Set α) (r : α → α → Prop) : s.chainHeight r = ⊤ ↔ ∀ (n : ℕ), ∃ t ⊆ s, t.encard = ↑n ∧ IsChain r t

@[simp]

theorem Set.chainHeight_eq_zero_iff {α : Type u_1} (s : Set α) (r : α → α → Prop) : s.chainHeight r = 0 ↔ s = ∅

@[simp]

theorem Set.chainHeight_empty {α : Type u_1} (r : α → α → Prop) : ∅.chainHeight r = 0

@[simp]

theorem Set.one_le_chainHeight_iff {α : Type u_1} (s : Set α) (r : α → α → Prop) : 1 ≤ s.chainHeight r ↔ s.Nonempty

@[simp]

theorem Set.chainHeight_of_isEmpty {α : Type u_1} (s : Set α) (r : α → α → Prop) [IsEmpty α] : s.chainHeight r = 0

theorem Set.chainHeight_mono {α : Type u_1} (r : α → α → Prop) (s t : Set α) (h : s ⊆ t) : s.chainHeight r ≤ t.chainHeight r

@[simp]

theorem Set.chainHeight_flip {α : Type u_1} (s : Set α) (r : α → α → Prop) : s.chainHeight (flip r) = s.chainHeight r

theorem Set.chainHeight_eq_of_relEmbedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} (s : Set α) (e : r ↪r r') : (⇑e '' s).chainHeight r' = s.chainHeight r

theorem Set.chainHeight_eq_of_relIso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} (s : Set α) (e : r ≃r r') : (⇑e '' s).chainHeight r' = s.chainHeight r

@[simp]

theorem Set.chainHeight_coe_univ {α : Type u_1} (s : Set α) (r : α → α → Prop) : (univ.chainHeight fun (x1 x2 : ↑s) => r ↑x1 ↑x2) = s.chainHeight r

@[simp]

theorem Set.chainHeight_coe_univ_le {α : Type u_1} (s : Set α) [LE α] : (univ.chainHeight fun (x1 x2 : ↑s) => x1 ≤ x2) = s.chainHeight fun (x1 x2 : α) => x1 ≤ x2

@[simp]

theorem Set.chainHeight_coe_univ_lt {α : Type u_1} (s : Set α) [LT α] : (univ.chainHeight fun (x1 x2 : ↑s) => x1 < x2) = s.chainHeight fun (x1 x2 : α) => x1 < x2