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ₖ. Then the range of f is a maximal chain.

We formulate this result in terms of IsMaxChain and Flag.

source

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 (Fin.castSucc k) ⩿ f (Fin.succ k))
 :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ₖ.
Then the range of f is a maximal chain.

source

@[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 (Fin.castSucc k) ⩿ f (Fin.succ k))
 :↑(Flag.rangeFin f h0 hlast hcovby) = Set.range f

source

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 (Fin.castSucc k) ⩿ f (Fin.succ k))
 :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ₖ.
Then the range of f is a Flag α.

Instances For

source

@[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 (Fin.castSucc k) ⩿ f (Fin.succ k)}
 :x ∈ Flag.rangeFin f h0 hlast hcovby ↔ ∃ k, f k = x

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

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