Range of f : Fin (n + 1) → α
as a Flag
#
Let f : Fin (n + 1) → α
be an (n + 1)
-tuple (f₀, …, fₙ)
such that
f₀ = ⊥
andfₙ = ⊤
;fₖ₊₁
weakly coversfₖ
for all0 ≤ k < n
; this means thatfₖ ≤ fₖ₊₁
and there is noc
such thatfₖ<c<fₖ₊₁
. Then the range off
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₀ = ⊥
andfₙ = ⊤
;fₖ₊₁
weakly coversfₖ
for all0 ≤ k < n
; this means thatfₖ ≤ fₖ₊₁
and there is noc
such thatfₖ<c<fₖ₊₁
. Then the range off
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₀ = ⊥
andfₙ = ⊤
;fₖ₊₁
weakly coversfₖ
for all0 ≤ k < n
; this means thatfₖ ≤ fₖ₊₁
and there is noc
such thatfₖ<c<fₖ₊₁
. Then the range off
is aFlag α
.
Equations
- Flag.rangeFin f h0 hlast hcovBy = { carrier := Set.range f, Chain' := ⋯, max_chain' := ⋯ }