α : Type ?u.45017
n : ℕ
A B : Finset (Fin n)
⊢ StrictMono fun i => ↑i
α : Type ?u.45017
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_le_iff _ _ _
no goals
α : Type ?u.45017
n : ℕ
A B : Finset (Fin n)
⊢ StrictMono fun i => ↑i
exact (fun x y k => k)