Documentation

Mathlib.Data.Fin.FlagRange

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

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

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.
@[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) :
(Flag.rangeFin f h0 hlast hcovBy) = Set.range f
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
Instances For
    @[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 Flag.rangeFin f h0 hlast hcovBy ∃ (k : Fin (n + 1)), f k = x