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ₖ
. 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 (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₀ = ⊥
andfₙ = ⊤
;fₖ₊₁
weakly coversfₖ
for all0 ≤ k < n
; this means thatfₖ ≤ fₖ₊₁
and there is noc
such thatfₖ
. 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 (Fin.castSucc k) ⩿ f (Fin.succ k))
:
↑(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 (Fin.castSucc k) ⩿ f (Fin.succ k))
:
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ₖ
. Then the range of f
is aFlag α
.
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 (Fin.castSucc k) ⩿ f (Fin.succ k)}
:
x ∈ Flag.rangeFin f h0 hlast hcovby ↔ ∃ k, f k = x