# 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} [] [] {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 (x x_1 : α) => x x_1) (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.
@[simp]
theorem Flag.rangeFin_carrier {α : Type u_1} [] [] {n : } (f : Fin (n + 1)α) (h0 : f 0 = ) (hlast : f (Fin.last n) = ) (hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ) :
(Flag.rangeFin f h0 hlast hcovBy) =
def Flag.rangeFin {α : Type u_1} [] [] {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 := , Chain' := , max_chain' := }
Instances For
@[simp]
theorem Flag.mem_rangeFin {α : Type u_1} [] [] {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 Flag.rangeFin f h0 hlast hcovBy ∃ (k : Fin (n + 1)), f k = x