Minimal and maximal layers of a set

This file defines Set.minLayer and Set.maxLayer as the sets obtained from iterated application of Minimal/Maximal on a set, excluding earlier layers.

Main declarations

• Set.minLayer (Set.maxLayer): the nth minimal (maximal) layer of the given set A.
• Set.pairwiseDisjoint_minLayer (Set.pairwiseDisjoint_maxLayer), Set.isAntichain_minLayer (Set.isAntichain_maxLayer): minimal (maximal) layers are pairwise disjoint antichains.
• Set.iUnion_minLayer_iff_bounded_series: if the length of LTSeries in A is bounded, A equals the union of its minLayers up to n.

@[irreducible]

def Set.minLayer {α : Type u_1} [PartialOrder α] (A : Set α) (n : ℕ) : Set α

The nth minimal layer of A.

Equations

• A.minLayer n = {a : α | Minimal (fun (x : α) => x ∈ A \ ⋃ (k : ℕ), ⋃ (_ : k < n), A.minLayer k) a}

def Set.maxLayer {α : Type u_1} [PartialOrder α] (A : Set α) (n : ℕ) : Set α

The nth maximal layer of A.

Equations

• A.maxLayer n = A.minLayer n

def Set.layersAbove {α : Type u_1} [PartialOrder α] (A : Set α) (n : ℕ) : Set α

The elements above A's n minimal layers.

Equations

• A.layersAbove n = A \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), A.minLayer k

def Set.layersBelow {α : Type u_1} [PartialOrder α] (A : Set α) (n : ℕ) : Set α

The elements below A's n maximal layers.

Equations

• A.layersBelow n = A \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), A.maxLayer k

theorem Set.maxLayer_def {α : Type u_1} [PartialOrder α] {A : Set α} {n : ℕ} : A.maxLayer n = {a : α | Maximal (fun (x : α) => x ∈ A \ ⋃ (k : ℕ), ⋃ (_ : k < n), A.maxLayer k) a}

theorem Set.minLayer_subset {α : Type u_1} [PartialOrder α] {A : Set α} {n : ℕ} : A.minLayer n ⊆ A

theorem Set.maxLayer_subset {α : Type u_1} [PartialOrder α] {A : Set α} {n : ℕ} : A.maxLayer n ⊆ A

theorem Set.layersAbove_subset {α : Type u_1} [PartialOrder α] {A : Set α} {n : ℕ} : A.layersAbove n ⊆ A

theorem Set.layersBelow_subset {α : Type u_1} [PartialOrder α] {A : Set α} {n : ℕ} : A.layersBelow n ⊆ A

theorem Set.minLayer_zero {α : Type u_1} [PartialOrder α] {A : Set α} : A.minLayer 0 = {a : α | Minimal (fun (x : α) => x ∈ A) a}

theorem Set.maxLayer_zero {α : Type u_1} [PartialOrder α] {A : Set α} : A.maxLayer 0 = {a : α | Maximal (fun (x : α) => x ∈ A) a}

theorem Set.disjoint_minLayer_of_ne {α : Type u_1} [PartialOrder α] {A : Set α} {m n : ℕ} (h : m ≠ n) : Disjoint (A.minLayer m) (A.minLayer n)

theorem Set.disjoint_maxLayer_of_ne {α : Type u_1} [PartialOrder α] {A : Set α} {m n : ℕ} (h : m ≠ n) : Disjoint (A.maxLayer m) (A.maxLayer n)

theorem Set.pairwiseDisjoint_minLayer {α : Type u_1} [PartialOrder α] {A : Set α} : univ.PairwiseDisjoint A.minLayer

theorem Set.pairwiseDisjoint_maxLayer {α : Type u_1} [PartialOrder α] {A : Set α} : univ.PairwiseDisjoint A.maxLayer

theorem Set.isAntichain_minLayer {α : Type u_1} [PartialOrder α] {A : Set α} {n : ℕ} : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) (A.minLayer n)

theorem Set.isAntichain_maxLayer {α : Type u_1} [PartialOrder α] {A : Set α} {n : ℕ} : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) (A.maxLayer n)

theorem Set.exists_le_in_minLayer_of_le {α : Type u_1} [PartialOrder α] {A : Set α} {m n : ℕ} {a : α} (ha : a ∈ A.minLayer n) (hm : m ≤ n) : ∃ c ∈ A.minLayer m, c ≤ a

theorem Set.exists_le_in_maxLayer_of_le {α : Type u_1} [PartialOrder α] {A : Set α} {m n : ℕ} {a : α} (ha : a ∈ A.maxLayer n) (hm : m ≤ n) : ∃ c ∈ A.maxLayer m, a ≤ c

theorem Set.subtype_mk_minimal_iff (α : Type u_2) [Preorder α] (s : Set α) (t : Set ↑s) (x : α) (hx : x ∈ s) : Minimal (fun (x : ↑s) => x ∈ t) ⟨x, hx⟩ ↔ Minimal (fun (y : α) => ∃ (h : y ∈ s), y ∈ s ∧ ⟨y, h⟩ ∈ t) x

theorem Set.minLayer_eq_setOf_height {α : Type u_1} [PartialOrder α] {A : Set α} {n : ℕ} : A.minLayer n = {x : α | ∃ (hx : x ∈ A), Order.height ⟨x, hx⟩ = ↑n}

A.minLayer n comprises exactly A's elements of height n.

theorem Set.iUnion_lt_minLayer_iff_bounded_series {α : Type u_1} [PartialOrder α] {A : Set α} {n : ℕ} : ⋃ (k : ℕ), ⋃ (_ : k < n), A.minLayer k = A ↔ ∀ (p : LTSeries ↑A), p.length < n

theorem Set.iUnion_minLayer_iff_bounded_series {α : Type u_1} [PartialOrder α] {A : Set α} {n : ℕ} : ⋃ (k : ℕ), ⋃ (_ : k ≤ n), A.minLayer k = A ↔ ∀ (p : LTSeries ↑A), p.length ≤ n

A equals the union of its minLayers up to n iff all LTSeries in A have length at most n.

theorem Set.exists_le_in_layersAbove_of_le {α : Type u_1} [PartialOrder α] {A : Set α} {m n : ℕ} {a : α} [Finite α] (ha : a ∈ A.layersAbove n) (hm : m ≤ n) : ∃ c ∈ A.minLayer m, c ≤ a

theorem Set.exists_le_in_layersBelow_of_le {α : Type u_1} [PartialOrder α] {A : Set α} {m n : ℕ} {a : α} [Finite α] (ha : a ∈ A.layersBelow n) (hm : m ≤ n) : ∃ c ∈ A.maxLayer m, a ≤ c