rainbow.math.sets.finset.range

setlike/membership

DefinitionSource, line 102

setlike/membership.{u, v} :
  (Container : Type v) (A : Type u) (dictionary : Container → A → Prop) (x₁ : Container)
  (x₂ : A)
  → Prop

finset/setlike

DefinitionSource, line 118

finset/setlike.{u} :
  (A : Type u) (x₁ : finset/Finset A) (x₂ : A)
  → Prop

order/less-than

DefinitionSource, line 138

order/less-than.{u} :
  (A : Type u) (dictionary : A → A → Prop) (x₁ x₂ : A)
  → Prop

order/less-or-equal

DefinitionSource, line 152

order/less-or-equal.{u} :
  (A : Type u) (dictionary : A → A → Prop) (x₁ x₂ : A)
  → Prop

nat/at-most

DefinitionSource, line 166

nat/at-most :
  (x₁ x₂ : ℕ)
  → Prop

ℕ = data/Nat

order/preorder-from-partial

DefinitionSource, line 181

order/preorder-from-partial.{u} :
  (A : Type u) (relation : A → A → Prop) (x₁ x₂ : A)
  → Prop

finset/partial-order

DefinitionSource, line 195

finset/partial-order.{u} :
  (A : Type u) (x₁ x₂ : finset/Finset A)
  → Prop

order/monotone

DefinitionSource, line 215

order/monotone.{u, v} :
  (A : Type u) (B : Type v) (source-order : A → A → Prop) (target-order : B → B → Prop)
  (mapping : A → B)
  → Prop

list/nat-range

DefinitionSource, line 83

list/nat-range :
  (x₁ : ℕ)
  → List ℕ

List = data/Listℕ = data/Nat

finset/range

DefinitionSource, line 381

finset/range :
  (x₁ : ℕ)
  → finset/Finset ℕ

ℕ = data/Nat

nat/member-range-successor-add

TheoremFor all inputsNo axiomsSource, line 247

nat/member-range-successor-add :
  (value extra : ℕ)
  → list/membership ℕ (list/nat-range (algebra/nat-add (data/succ value) extra)) value

ℕ = data/Nat

nat/below-member-range

TheoremFor all inputsNo axiomsSource, line 315

nat/below-member-range :
  (value upper : ℕ) (evidence : nat/strict-below value upper)
  → list/membership ℕ (list/nat-range upper) value

ℕ = data/Nat

finset/member-range-equivalent-below

TheoremFor all inputsNo axiomsSource, line 396

finset/member-range-equivalent-below :
  (value upper : ℕ)
  → proposition/conjunction (set → nat/strict-below value upper) (nat/strict-below value upper → set)
  where set := finset/to-set ℕ (finset/range upper) value

ℕ = data/Nat

finset/exists-nat-subset-range

TheoremFor all inputsNo axiomsSource, line 423

finset/exists-nat-subset-range :
  (source : finset/Finset ℕ)
  → proposition/existence ℕ (fun upper => finset/subset ℕ source (finset/range upper))

ℕ = data/Nat

nat/not-strictly-below-self

TheoremFor all inputsNo axiomsSource, line 451

nat/not-strictly-below-self :
  (value : ℕ) (x₁ : nat/strict-below value value)
  → proposition/falsity

ℕ = data/Nat

finset/not-member-range-self

TheoremFor all inputsNo axiomsSource, line 478

finset/not-member-range-self :
  (value : ℕ) (x₁ : finset/to-set ℕ (finset/range value) value)
  → proposition/falsity

ℕ = data/Nat

finset/member-range-proposition-equality

TheoremHolds by unfolding a definitionNo axiomsSource, line 496

finset/member-range-proposition-equality :
  (upper value : ℕ)
  → finset/to-set ℕ (finset/range upper) value = nat/strict-below value upper

= = equality/Eqℕ = data/Nat

finset/range-subset-of-at-most

TheoremFor all inputsNo axiomsSource, line 510

finset/range-subset-of-at-most :
  (left right : ℕ)
  (ordered : left ≤ right)
  → finset/subset ℕ (finset/range left) (finset/range right)

ℕ = data/Nat≤ = nat/at-most

finset/at-most-of-range-subset

TheoremFor all inputsNo axiomsSource, line 588

finset/at-most-of-range-subset :
  (left right : ℕ) (included : finset/subset ℕ (finset/range left) (finset/range right))
  → left ≤ right

ℕ = data/Nat≤ = nat/at-most

finset/range-subset-equivalent-at-most

TheoremFor all inputsNo axiomsSource, line 636

finset/range-subset-equivalent-at-most :
  (left right : ℕ)
  → proposition/conjunction (subset → left ≤ right) (left ≤ right → subset)
  where subset := finset/subset ℕ (finset/range left) (finset/range right)

ℕ = data/Nat≤ = nat/at-most

finset/range-monotone

TheoremWorked exampleNo axiomsSource, line 660

finset/range-monotone :
  → order/monotone ℕ (finset/Finset ℕ) nat/at-most (finset/partial-order ℕ) finset/range

ℕ = data/Nat