Ordered

Main definitions

• FooBar

Main statements

• fooBar_unique

theorem Finset.mem_map_univ_asEmbedding {α : Type u_3} {β : Type u_4} [Fintype α] {p : β → Prop} (e : α ≃ Subtype p) {b : β} : b ∈ Finset.map e.asEmbedding Finset.univ ↔ p b

noncomputable def Finset.ordered {α : Type u_1} (J : Finset α) : Fin J.card ↪ α

An ordering of the elements of a finset.

Equations

• J.ordered = J.equivFin.symm.asEmbedding

theorem Finset.ordered_mem {α : Type u_1} {J : Finset α} (n : Fin J.card) : J.ordered n ∈ J

theorem Finset.map_ordered {α : Type u_1} (J : Finset α) : Finset.map J.ordered Finset.univ = J

theorem Finset.sum_ordered {α : Type u_1} {β : Type u_2} [AddCommMonoid β] (J : Finset α) (m : α → β) : ∑ i : Fin J.card, m (J.ordered i) = ∑ u ∈ J, m u

noncomputable def Finset.finsetLT {α : Type u_1} (J : Finset α) : Fin J.card → Finset α

The n first elements in J.ordered.

Equations

• J.finsetLT n = Finset.map J.ordered (Finset.filter (fun (j : Fin J.card) => j < n) Finset.univ)

@[simp]

theorem Finset.mem_finsetLT {α : Type u_1} (J : Finset α) (n : Fin J.card) (s : α) : s ∈ J.finsetLT n ↔ ∃ m < n, s = J.ordered m

theorem Finset.ordered_mem_finsetLT {α : Type u_1} (J : Finset α) {n : Fin J.card} {m : Fin J.card} (hnm : n < m) : J.ordered n ∈ J.finsetLT m

@[simp]

theorem Finset.finsetLT_zero {α : Type u_1} {J : Finset α} (hJ : 0 < J.card) : J.finsetLT ⟨0, hJ⟩ = ∅

theorem Finset.finsetLT_mono {α : Type u_1} (J : Finset α) : Monotone J.finsetLT

theorem Finset.finsetLT_subset {α : Type u_1} (J : Finset α) (n : Fin J.card) : J.finsetLT n ⊆ J

theorem Finset.biUnion_finsetLT {α : Type u_1} (J : Finset α) (n : Fin J.card) : ⋃ (i : Fin J.card), ⋃ (_ : i ≤ n), ↑(J.finsetLT i) = ↑(J.finsetLT n)

theorem Finset.iUnion_ordered {α : Type u_1} (J : Finset (Set α)) : ⋃ (i : Fin J.card), J.ordered i = ⋃₀ ↑J

theorem Finset.finsetLT_subset' {α : Type u_1} {C : Set (Set α)} (J : Finset (Set α)) (hJ : ↑J ⊆ C) (n : Fin J.card) : ↑(J.finsetLT n) ⊆ C

theorem Finset.sUnion_finsetLT_eq_biUnion {α : Type u_1} (J : Finset (Set α)) (n : Fin J.card) : ⋃₀ ↑(J.finsetLT n) = ⋃ (i : Fin J.card), ⋃ (_ : i < n), J.ordered i