α : Type ?u.6170
n : ℕ
A B : Finset (Fin n)
⊢ StrictMono fun i => ↑i
α : Type ?u.6170
n : ℕ
A B : Finset (Fin n)
⊢ toColex (image (fun i => ↑i) A) < toColex (image (fun i => ↑i) B) ↔ toColex A < toColex B
refine' Colex.hom_lt_iff _ _ _
no goals
α : Type ?u.6170
n : ℕ
A B : Finset (Fin n)
⊢ StrictMono fun i => ↑i
exact (fun x y k => k)