Range of f : Fin (n + 1) → α as a Flag

Let f : Fin (n + 1) → α be an (n + 1)-tuple (f₀, …, fₙ) such that

• f₀ = ⊥ and fₙ = ⊤;
• fₖ₊₁ weakly covers fₖ for all 0 ≤ k < n; this means that fₖ ≤ fₖ₊₁ and there is no c such that fₖ<c<fₖ₊₁.

Then the range of f is a maximal chain.

We formulate this result in terms of IsMaxChain and Flag.

theorem IsMaxChain.range_fin_of_covBy {α : Type u_1} [PartialOrder α] [BoundedOrder α] {n : ℕ} {f : Fin (n + 1) → α} (h0 : f 0 = ⊥) (hlast : f (Fin.last n) = ⊤) (hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ) : IsMaxChain (fun (x1 x2 : α) => x1 ≤ x2) (Set.range f)

Let f : Fin (n + 1) → α be an (n + 1)-tuple (f₀, …, fₙ) such that

• f₀ = ⊥ and fₙ = ⊤;
• fₖ₊₁ weakly covers fₖ for all 0 ≤ k < n; this means that fₖ ≤ fₖ₊₁ and there is no c such that fₖ<c<fₖ₊₁.

Then the range of f is a maximal chain.

def Flag.rangeFin {α : Type u_1} [PartialOrder α] [BoundedOrder α] {n : ℕ} (f : Fin (n + 1) → α) (h0 : f 0 = ⊥) (hlast : f (Fin.last n) = ⊤) (hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ) : Flag α

Let f : Fin (n + 1) → α be an (n + 1)-tuple (f₀, …, fₙ) such that

• f₀ = ⊥ and fₙ = ⊤;
• fₖ₊₁ weakly covers fₖ for all 0 ≤ k < n; this means that fₖ ≤ fₖ₊₁ and there is no c such that fₖ<c<fₖ₊₁.

Then the range of f is a Flag α.

Equations

• Flag.rangeFin f h0 hlast hcovBy = { carrier := Set.range f, Chain' := ⋯, max_chain' := ⋯ }

@[simp]

theorem Flag.rangeFin_carrier {α : Type u_1} [PartialOrder α] [BoundedOrder α] {n : ℕ} (f : Fin (n + 1) → α) (h0 : f 0 = ⊥) (hlast : f (Fin.last n) = ⊤) (hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ) : ↑(rangeFin f h0 hlast hcovBy) = Set.range f

@[simp]

theorem Flag.mem_rangeFin {α : Type u_1} [PartialOrder α] [BoundedOrder α] {n : ℕ} {f : Fin (n + 1) → α} {x : α} {h0 : f 0 = ⊥} {hlast : f (Fin.last n) = ⊤} {hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ} : x ∈ rangeFin f h0 hlast hcovBy ↔ ∃ (k : Fin (n + 1)), f k = x