Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2021 YaΓ«l Dillies, Bhavik Mehta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: YaΓ«l Dillies, Bhavik Mehta

! This file was ported from Lean 3 source module data.set.equitable
! leanprover-community/mathlib commit 8631e2d5ea77f6c13054d9151d82b83069680cb1
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.BigOperators.Order
import Mathlib.Data.Nat.Basic

/-!
# Equitable functions

This file defines equitable functions.

A function `f` is equitable on a set `s` if `f a₁ ≀ f aβ‚‚ + 1` for all `a₁, aβ‚‚ ∈ s`. This is mostly
useful when the codomain of `f` is `β„•` or `β„€` (or more generally a successor order).

## TODO

`β„•` can be replaced by any `SuccOrder` + `ConditionallyCompleteMonoid`, but we don't have the
latter yet.
-/


open BigOperators

variable {
Ξ±: Type ?u.2
Ξ±
Ξ²: Type ?u.5
Ξ²
:
Type _: Type (?u.2+1)
Type _
} namespace Set /-- A set is equitable if no element value is more than one bigger than another. -/ def
EquitableOn: [inst : LE Ξ²] β†’ [inst : Add Ξ²] β†’ [inst : One Ξ²] β†’ Set Ξ± β†’ (Ξ± β†’ Ξ²) β†’ Prop
EquitableOn
[
LE: Type ?u.14 β†’ Type ?u.14
LE
Ξ²: Type ?u.11
Ξ²
] [
Add: Type ?u.17 β†’ Type ?u.17
Add
Ξ²: Type ?u.11
Ξ²
] [
One: Type ?u.20 β†’ Type ?u.20
One
Ξ²: Type ?u.11
Ξ²
] (
s: Set Ξ±
s
:
Set: Type ?u.23 β†’ Type ?u.23
Set
Ξ±: Type ?u.8
Ξ±
) (
f: Ξ± β†’ Ξ²
f
:
Ξ±: Type ?u.8
Ξ±
β†’
Ξ²: Type ?u.11
Ξ²
) :
Prop: Type
Prop
:= βˆ€ ⦃
a₁: ?m.37
a₁
aβ‚‚: ?m.40
aβ‚‚
⦄,
a₁: ?m.37
a₁
∈
s: Set Ξ±
s
β†’
aβ‚‚: ?m.40
aβ‚‚
∈
s: Set Ξ±
s
β†’
f: Ξ± β†’ Ξ²
f
a₁: ?m.37
a₁
≀
f: Ξ± β†’ Ξ²
f
aβ‚‚: ?m.40
aβ‚‚
+
1: ?m.107
1
#align set.equitable_on
Set.EquitableOn: {Ξ± : Type u_1} β†’ {Ξ² : Type u_2} β†’ [inst : LE Ξ²] β†’ [inst : Add Ξ²] β†’ [inst : One Ξ²] β†’ Set Ξ± β†’ (Ξ± β†’ Ξ²) β†’ Prop
Set.EquitableOn
@[simp] theorem
equitableOn_empty: βˆ€ [inst : LE Ξ²] [inst_1 : Add Ξ²] [inst_2 : One Ξ²] (f : Ξ± β†’ Ξ²), EquitableOn βˆ… f
equitableOn_empty
[
LE: Type ?u.222 β†’ Type ?u.222
LE
Ξ²: Type ?u.219
Ξ²
] [
Add: Type ?u.225 β†’ Type ?u.225
Add
Ξ²: Type ?u.219
Ξ²
] [
One: Type ?u.228 β†’ Type ?u.228
One
Ξ²: Type ?u.219
Ξ²
] (
f: Ξ± β†’ Ξ²
f
:
Ξ±: Type ?u.216
Ξ±
β†’
Ξ²: Type ?u.219
Ξ²
) :
EquitableOn: {Ξ± : Type ?u.236} β†’ {Ξ² : Type ?u.235} β†’ [inst : LE Ξ²] β†’ [inst : Add Ξ²] β†’ [inst : One Ξ²] β†’ Set Ξ± β†’ (Ξ± β†’ Ξ²) β†’ Prop
EquitableOn
βˆ…: ?m.310
βˆ…
f: Ξ± β†’ Ξ²
f
:= fun
a: ?m.392
a
_: ?m.395
_
ha: ?m.398
ha
=> (
Set.not_mem_empty: βˆ€ {Ξ± : Type ?u.400} (x : Ξ±), Β¬x ∈ βˆ…
Set.not_mem_empty
a: ?m.392
a
ha: ?m.398
ha
).
elim: βˆ€ {C : Sort ?u.402}, False β†’ C
elim
#align set.equitable_on_empty
Set.equitableOn_empty: βˆ€ {Ξ± : Type u_2} {Ξ² : Type u_1} [inst : LE Ξ²] [inst_1 : Add Ξ²] [inst_2 : One Ξ²] (f : Ξ± β†’ Ξ²), EquitableOn βˆ… f
Set.equitableOn_empty
theorem
equitableOn_iff_exists_le_le_add_one: βˆ€ {s : Set Ξ±} {f : Ξ± β†’ β„•}, EquitableOn s f ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
equitableOn_iff_exists_le_le_add_one
{
s: Set Ξ±
s
:
Set: Type ?u.459 β†’ Type ?u.459
Set
Ξ±: Type ?u.453
Ξ±
} {
f: Ξ± β†’ β„•
f
:
Ξ±: Type ?u.453
Ξ±
β†’
β„•: Type
β„•
} :
s: Set Ξ±
s
.
EquitableOn: {Ξ± : Type ?u.467} β†’ {Ξ² : Type ?u.466} β†’ [inst : LE Ξ²] β†’ [inst : Add Ξ²] β†’ [inst : One Ξ²] β†’ Set Ξ± β†’ (Ξ± β†’ Ξ²) β†’ Prop
EquitableOn
f: Ξ± β†’ β„•
f
↔ βˆƒ
b: ?m.514
b
, βˆ€
a: ?m.517
a
∈
s: Set Ξ±
s
,
b: ?m.514
b
≀
f: Ξ± β†’ β„•
f
a: ?m.517
a
∧
f: Ξ± β†’ β„•
f
a: ?m.517
a
≀
b: ?m.514
b
+
1: ?m.559
1
:=

Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•


EquitableOn s f ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•


EquitableOn s f β†’ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•


EquitableOn s f ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

f: Ξ± β†’ β„•


inl
EquitableOn βˆ… f β†’ βˆƒ b, βˆ€ (a : Ξ±), a ∈ βˆ… β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•

x: Ξ±

hx: x ∈ s


inr.intro
EquitableOn s f β†’ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•


EquitableOn s f ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

f: Ξ± β†’ β„•


inl
EquitableOn βˆ… f β†’ βˆƒ b, βˆ€ (a : Ξ±), a ∈ βˆ… β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

f: Ξ± β†’ β„•


inl
EquitableOn βˆ… f β†’ βˆƒ b, βˆ€ (a : Ξ±), a ∈ βˆ… β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•

x: Ξ±

hx: x ∈ s


inr.intro
EquitableOn s f β†’ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1

Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•


EquitableOn s f ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•

x: Ξ±

hx: x ∈ s

hs: EquitableOn s f


inr.intro
βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•


EquitableOn s f ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•

x: Ξ±

hx: x ∈ s

hs: EquitableOn s f

h: βˆ€ (y : Ξ±), y ∈ s β†’ f x ≀ f y


pos
βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•

x: Ξ±

hx: x ∈ s

hs: EquitableOn s f

h: Β¬βˆ€ (y : Ξ±), y ∈ s β†’ f x ≀ f y


neg
βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•


EquitableOn s f ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•

x: Ξ±

hx: x ∈ s

hs: EquitableOn s f

h: βˆ€ (y : Ξ±), y ∈ s β†’ f x ≀ f y


pos
βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•

x: Ξ±

hx: x ∈ s

hs: EquitableOn s f

h: βˆ€ (y : Ξ±), y ∈ s β†’ f x ≀ f y


pos
βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•

x: Ξ±

hx: x ∈ s

hs: EquitableOn s f

h: Β¬βˆ€ (y : Ξ±), y ∈ s β†’ f x ≀ f y


neg
βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1

Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•


EquitableOn s f ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•

x: Ξ±

hx: x ∈ s

hs: EquitableOn s f

h: βˆƒ y, y ∈ s ∧ f y < f x


neg
βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•


EquitableOn s f ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•

x: Ξ±

hx: x ∈ s

hs: EquitableOn s f

w: Ξ±

hw: w ∈ s

hwx: f w < f x


neg.intro.intro
βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•


EquitableOn s f ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•

x: Ξ±

hx: x ∈ s

hs: EquitableOn s f

w: Ξ±

hw: w ∈ s

hwx: f w < f x

y: Ξ±

hy: y ∈ s


neg.intro.intro
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•


EquitableOn s f ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•

x: Ξ±

hx: x ∈ s

hs: EquitableOn s f

w: Ξ±

hw: w ∈ s

hwx: f w < f x

y: Ξ±

hy: y ∈ s


neg.intro.intro
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•

x: Ξ±

hx: x ∈ s

hs: EquitableOn s f

w: Ξ±

hw: w ∈ s

hwx: f w < f x

y: Ξ±

hy: y ∈ s


neg.intro.intro
f x ≀ Nat.succ (f y)
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•

x: Ξ±

hx: x ∈ s

hs: EquitableOn s f

w: Ξ±

hw: w ∈ s

hwx: f w < f x

y: Ξ±

hy: y ∈ s


neg.intro.intro
f x ≀ Nat.succ (f y)
Ξ±: Type u_1

Ξ²: Type ?u.456

s: Set Ξ±

f: Ξ± β†’ β„•


EquitableOn s f ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1

Goals accomplished! πŸ™
#align set.equitable_on_iff_exists_le_le_add_one
Set.equitableOn_iff_exists_le_le_add_one: βˆ€ {Ξ± : Type u_1} {s : Set Ξ±} {f : Ξ± β†’ β„•}, EquitableOn s f ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Set.equitableOn_iff_exists_le_le_add_one
theorem
equitableOn_iff_exists_image_subset_icc: βˆ€ {s : Set Ξ±} {f : Ξ± β†’ β„•}, EquitableOn s f ↔ βˆƒ b, f '' s βŠ† Icc b (b + 1)
equitableOn_iff_exists_image_subset_icc
{
s: Set Ξ±
s
:
Set: Type ?u.4646 β†’ Type ?u.4646
Set
Ξ±: Type ?u.4640
Ξ±
} {
f: Ξ± β†’ β„•
f
:
Ξ±: Type ?u.4640
Ξ±
β†’
β„•: Type
β„•
} :
s: Set Ξ±
s
.
EquitableOn: {Ξ± : Type ?u.4654} β†’ {Ξ² : Type ?u.4653} β†’ [inst : LE Ξ²] β†’ [inst : Add Ξ²] β†’ [inst : One Ξ²] β†’ Set Ξ± β†’ (Ξ± β†’ Ξ²) β†’ Prop
EquitableOn
f: Ξ± β†’ β„•
f
↔ βˆƒ
b: ?m.4701
b
,
f: Ξ± β†’ β„•
f
''
s: Set Ξ±
s
βŠ†
Icc: {Ξ± : Type ?u.4717} β†’ [inst : Preorder Ξ±] β†’ Ξ± β†’ Ξ± β†’ Set Ξ±
Icc
b: ?m.4701
b
(
b: ?m.4701
b
+
1: ?m.4749
1
) :=

Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.4643

s: Set Ξ±

f: Ξ± β†’ β„•


EquitableOn s f ↔ βˆƒ b, f '' s βŠ† Icc b (b + 1)

Goals accomplished! πŸ™
#align set.equitable_on_iff_exists_image_subset_Icc
Set.equitableOn_iff_exists_image_subset_icc: βˆ€ {Ξ± : Type u_1} {s : Set Ξ±} {f : Ξ± β†’ β„•}, EquitableOn s f ↔ βˆƒ b, f '' s βŠ† Icc b (b + 1)
Set.equitableOn_iff_exists_image_subset_icc
theorem
equitableOn_iff_exists_eq_eq_add_one: βˆ€ {Ξ± : Type u_1} {s : Set Ξ±} {f : Ξ± β†’ β„•}, EquitableOn s f ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ f a = b ∨ f a = b + 1
equitableOn_iff_exists_eq_eq_add_one
{
s: Set Ξ±
s
:
Set: Type ?u.5349 β†’ Type ?u.5349
Set
Ξ±: Type ?u.5343
Ξ±
} {
f: Ξ± β†’ β„•
f
:
Ξ±: Type ?u.5343
Ξ±
β†’
β„•: Type
β„•
} :
s: Set Ξ±
s
.
EquitableOn: {Ξ± : Type ?u.5357} β†’ {Ξ² : Type ?u.5356} β†’ [inst : LE Ξ²] β†’ [inst : Add Ξ²] β†’ [inst : One Ξ²] β†’ Set Ξ± β†’ (Ξ± β†’ Ξ²) β†’ Prop
EquitableOn
f: Ξ± β†’ β„•
f
↔ βˆƒ
b: ?m.5404
b
, βˆ€
a: ?m.5407
a
∈
s: Set Ξ±
s
,
f: Ξ± β†’ β„•
f
a: ?m.5407
a
=
b: ?m.5404
b
∨
f: Ξ± β†’ β„•
f
a: ?m.5407
a
=
b: ?m.5404
b
+
1: ?m.5448
1
:=

Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.5346

s: Set Ξ±

f: Ξ± β†’ β„•


EquitableOn s f ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ f a = b ∨ f a = b + 1
Ξ±: Type u_1

Ξ²: Type ?u.5346

s: Set Ξ±

f: Ξ± β†’ β„•


EquitableOn s f ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ f a = b ∨ f a = b + 1
Ξ±: Type u_1

Ξ²: Type ?u.5346

s: Set Ξ±

f: Ξ± β†’ β„•


(βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1) ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ f a = b ∨ f a = b + 1
Ξ±: Type u_1

Ξ²: Type ?u.5346

s: Set Ξ±

f: Ξ± β†’ β„•


EquitableOn s f ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ f a = b ∨ f a = b + 1

Goals accomplished! πŸ™

Goals accomplished! πŸ™
#align set.equitable_on_iff_exists_eq_eq_add_one
Set.equitableOn_iff_exists_eq_eq_add_one: βˆ€ {Ξ± : Type u_1} {s : Set Ξ±} {f : Ξ± β†’ β„•}, EquitableOn s f ↔ βˆƒ b, βˆ€ (a : Ξ±), a ∈ s β†’ f a = b ∨ f a = b + 1
Set.equitableOn_iff_exists_eq_eq_add_one
section OrderedSemiring variable [
OrderedSemiring: Type ?u.6182 β†’ Type ?u.6182
OrderedSemiring
Ξ²: Type ?u.6179
Ξ²
] theorem
Subsingleton.equitableOn: βˆ€ {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : OrderedSemiring Ξ²] {s : Set Ξ±}, Set.Subsingleton s β†’ βˆ€ (f : Ξ± β†’ Ξ²), EquitableOn s f
Subsingleton.equitableOn
{
s: Set Ξ±
s
:
Set: Type ?u.6185 β†’ Type ?u.6185
Set
Ξ±: Type ?u.6176
Ξ±
} (hs :
s: Set Ξ±
s
.
Subsingleton: {Ξ± : Type ?u.6188} β†’ Set Ξ± β†’ Prop
Subsingleton
) (
f: Ξ± β†’ Ξ²
f
:
Ξ±: Type ?u.6176
Ξ±
β†’
Ξ²: Type ?u.6179
Ξ²
) :
s: Set Ξ±
s
.
EquitableOn: {Ξ± : Type ?u.6200} β†’ {Ξ² : Type ?u.6199} β†’ [inst : LE Ξ²] β†’ [inst : Add Ξ²] β†’ [inst : One Ξ²] β†’ Set Ξ± β†’ (Ξ± β†’ Ξ²) β†’ Prop
EquitableOn
f: Ξ± β†’ Ξ²
f
:= fun
i: ?m.6687
i
j: ?m.6690
j
hi: ?m.6693
hi
hj: ?m.6696
hj
=>

Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: OrderedSemiring β

s: Set Ξ±

hs: Set.Subsingleton s

f: Ξ± β†’ Ξ²

i, j: Ξ±

hi: i ∈ s

hj: j ∈ s


f i ≀ f j + 1
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: OrderedSemiring β

s: Set Ξ±

hs: Set.Subsingleton s

f: Ξ± β†’ Ξ²

i, j: Ξ±

hi: i ∈ s

hj: j ∈ s


f i ≀ f j + 1
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: OrderedSemiring β

s: Set Ξ±

hs: Set.Subsingleton s

f: Ξ± β†’ Ξ²

i, j: Ξ±

hi: i ∈ s

hj: j ∈ s


f j ≀ f j + 1
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: OrderedSemiring β

s: Set Ξ±

hs: Set.Subsingleton s

f: Ξ± β†’ Ξ²

i, j: Ξ±

hi: i ∈ s

hj: j ∈ s


f j ≀ f j + 1
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: OrderedSemiring β

s: Set Ξ±

hs: Set.Subsingleton s

f: Ξ± β†’ Ξ²

i, j: Ξ±

hi: i ∈ s

hj: j ∈ s


f i ≀ f j + 1

Goals accomplished! πŸ™
#align set.subsingleton.equitable_on
Set.Subsingleton.equitableOn: βˆ€ {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : OrderedSemiring Ξ²] {s : Set Ξ±}, Set.Subsingleton s β†’ βˆ€ (f : Ξ± β†’ Ξ²), EquitableOn s f
Set.Subsingleton.equitableOn
theorem
equitableOn_singleton: βˆ€ {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : OrderedSemiring Ξ²] (a : Ξ±) (f : Ξ± β†’ Ξ²), EquitableOn {a} f
equitableOn_singleton
(
a: Ξ±
a
:
Ξ±: Type ?u.7729
Ξ±
) (
f: Ξ± β†’ Ξ²
f
:
Ξ±: Type ?u.7729
Ξ±
β†’
Ξ²: Type ?u.7732
Ξ²
) :
Set.EquitableOn: {Ξ± : Type ?u.7745} β†’ {Ξ² : Type ?u.7744} β†’ [inst : LE Ξ²] β†’ [inst : Add Ξ²] β†’ [inst : One Ξ²] β†’ Set Ξ± β†’ (Ξ± β†’ Ξ²) β†’ Prop
Set.EquitableOn
{
a: Ξ±
a
}
f: Ξ± β†’ Ξ²
f
:=
Set.subsingleton_singleton: βˆ€ {Ξ± : Type ?u.8252} {a : Ξ±}, Set.Subsingleton {a}
Set.subsingleton_singleton
.
equitableOn: βˆ€ {Ξ± : Type ?u.8255} {Ξ² : Type ?u.8256} [inst : OrderedSemiring Ξ²] {s : Set Ξ±}, Set.Subsingleton s β†’ βˆ€ (f : Ξ± β†’ Ξ²), EquitableOn s f
equitableOn
f: Ξ± β†’ Ξ²
f
#align set.equitable_on_singleton
Set.equitableOn_singleton: βˆ€ {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : OrderedSemiring Ξ²] (a : Ξ±) (f : Ξ± β†’ Ξ²), EquitableOn {a} f
Set.equitableOn_singleton
end OrderedSemiring end Set open Set namespace Finset variable {
s: Finset Ξ±
s
:
Finset: Type ?u.8324 β†’ Type ?u.8324
Finset
Ξ±: Type ?u.8318
Ξ±
} {
f: Ξ± β†’ β„•
f
:
Ξ±: Type ?u.11132
Ξ±
β†’
β„•: Type
β„•
} {
a: Ξ±
a
:
Ξ±: Type ?u.8303
Ξ±
} theorem
equitableOn_iff_le_le_add_one: βˆ€ {Ξ± : Type u_1} {s : Finset Ξ±} {f : Ξ± β†’ β„•}, EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
equitableOn_iff_le_le_add_one
:
EquitableOn: {Ξ± : Type ?u.8334} β†’ {Ξ² : Type ?u.8333} β†’ [inst : LE Ξ²] β†’ [inst : Add Ξ²] β†’ [inst : One Ξ²] β†’ Set Ξ± β†’ (Ξ± β†’ Ξ²) β†’ Prop
EquitableOn
(
s: Finset Ξ±
s
:
Set: Type ?u.8341 β†’ Type ?u.8341
Set
Ξ±: Type ?u.8318
Ξ±
)
f: Ξ± β†’ β„•
f
↔ βˆ€
a: ?m.8474
a
∈
s: Finset Ξ±
s
, (βˆ‘
i: ?m.8517
i
in
s: Finset Ξ±
s
,
f: Ξ± β†’ β„•
f
i: ?m.8517
i
) /
s: Finset Ξ±
s
.
card: {Ξ± : Type ?u.8531} β†’ Finset Ξ± β†’ β„•
card
≀
f: Ξ± β†’ β„•
f
a: ?m.8474
a
∧
f: Ξ± β†’ β„•
f
a: ?m.8474
a
≀ (βˆ‘
i: ?m.8602
i
in
s: Finset Ξ±
s
,
f: Ξ± β†’ β„•
f
i: ?m.8602
i
) /
s: Finset Ξ±
s
.
card: {Ξ± : Type ?u.8605} β†’ Finset Ξ± β†’ β„•
card
+
1: ?m.8610
1
:=

Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


(βˆƒ b, βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1) ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


(βˆƒ b, βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1) ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


(βˆƒ b, βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1) β†’ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1


intro
βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

h: βˆ€ (a : Ξ±), a ∈ s β†’ f a = b + 1


pos
βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

h: Β¬βˆ€ (a : Ξ±), a ∈ s β†’ f a = b + 1


neg
βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

h: βˆ€ (a : Ξ±), a ∈ s β†’ f a = b + 1


pos
βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

h: βˆ€ (a : Ξ±), a ∈ s β†’ f a = b + 1


pos
βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

h: Β¬βˆ€ (a : Ξ±), a ∈ s β†’ f a = b + 1


neg
βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a✝: α

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

h: βˆ€ (a : Ξ±), a ∈ s β†’ f a = b + 1

a: Ξ±

ha: a ∈ s


pos
(βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

h: βˆ€ (a : Ξ±), a ∈ s β†’ f a = b + 1


pos
βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a✝: α

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

h: βˆ€ (a : Ξ±), a ∈ s β†’ f a = b + 1

a: Ξ±

ha: a ∈ s


pos
(βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a✝: α

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

h: βˆ€ (a : Ξ±), a ∈ s β†’ f a = b + 1

a: Ξ±

ha: a ∈ s


pos
(βˆ‘ i in s, f i) / card s ≀ b + 1 ∧ b + 1 ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a✝: α

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

h: βˆ€ (a : Ξ±), a ∈ s β†’ f a = b + 1

a: Ξ±

ha: a ∈ s


pos
(βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a✝: α

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

h: βˆ€ (a : Ξ±), a ∈ s β†’ f a = b + 1

a: Ξ±

ha: a ∈ s


pos
card s * (b + 1) / card s ≀ b + 1 ∧ b + 1 ≀ card s * (b + 1) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a✝: α

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

h: βˆ€ (a : Ξ±), a ∈ s β†’ f a = b + 1

a: Ξ±

ha: a ∈ s


pos
(βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a✝: α

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

h: βˆ€ (a : Ξ±), a ∈ s β†’ f a = b + 1

a: Ξ±

ha: a ∈ s


pos
b + 1 ≀ b + 1 ∧ b + 1 ≀ b + 1 + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a✝: α

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

h: βˆ€ (a : Ξ±), a ∈ s β†’ f a = b + 1

a: Ξ±

ha: a ∈ s


pos
b + 1 ≀ b + 1 ∧ b + 1 ≀ b + 1 + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

h: βˆ€ (a : Ξ±), a ∈ s β†’ f a = b + 1


pos
βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1

Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

h: βˆƒ a, a ∈ s ∧ f a β‰  b + 1


neg
βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1


neg.intro.intro
βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1

h: b = (βˆ‘ i in s, f i) / card s


neg.intro.intro
βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1


h
b = (βˆ‘ i in s, f i) / card s
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1

h: b = (βˆ‘ i in s, f i) / card s


neg.intro.intro
βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1

h: b = (βˆ‘ i in s, f i) / card s


neg.intro.intro
βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1


h
b = (βˆ‘ i in s, f i) / card s
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1

h: b = (βˆ‘ i in s, f i) / card s


neg.intro.intro
βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1

h: b = (βˆ‘ i in s, f i) / card s


neg.intro.intro
βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1

h: b = (βˆ‘ i in s, f i) / card s


neg.intro.intro
βˆ€ (a : Ξ±), a ∈ s β†’ b ≀ f a ∧ f a ≀ b + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1

h: b = (βˆ‘ i in s, f i) / card s


neg.intro.intro
βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1

Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1


h
(βˆ‘ i in s, f i) / card s = b
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1


h
(βˆ‘ i in s, f i) / card s = b

Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1


b * card s ≀ βˆ‘ i in s, b

Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1


h
βˆ‘ i in s, (b + 1) ≀ Nat.succ b * card s
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1


h
βˆ‘ i in s, (b + 1) ≀ Nat.succ b * card s
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1


h
βˆ‘ i in s, (b + 1) ≀ card s * Nat.succ b
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1


h
βˆ‘ i in s, (b + 1) ≀ Nat.succ b * card s
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1


h
card s * ?m.11012 ≀ card s * Nat.succ b
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1


h
βˆ€ (x : Ξ±), x ∈ s β†’ b + 1 = ?m.11012
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1


Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±

b: β„•

hb: βˆ€ (a : Ξ±), a ∈ ↑s β†’ b ≀ f a ∧ f a ≀ b + 1

x: Ξ±

hx₁: x ∈ s

hxβ‚‚: f x β‰  b + 1


h
βˆ€ (x : Ξ±), x ∈ s β†’ b + 1 = Nat.succ b
Ξ±: Type u_1

Ξ²: Type ?u.8321

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1

Goals accomplished! πŸ™
#align finset.equitable_on_iff_le_le_add_one
Finset.equitableOn_iff_le_le_add_one: βˆ€ {Ξ± : Type u_1} {s : Finset Ξ±} {f : Ξ± β†’ β„•}, EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Finset.equitableOn_iff_le_le_add_one
theorem
EquitableOn.le: EquitableOn (↑s) f β†’ a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a
EquitableOn.le
(
h: EquitableOn (↑s) f
h
:
EquitableOn: {Ξ± : Type ?u.11148} β†’ {Ξ² : Type ?u.11147} β†’ [inst : LE Ξ²] β†’ [inst : Add Ξ²] β†’ [inst : One Ξ²] β†’ Set Ξ± β†’ (Ξ± β†’ Ξ²) β†’ Prop
EquitableOn
(
s: Finset Ξ±
s
:
Set: Type ?u.11225 β†’ Type ?u.11225
Set
Ξ±: Type ?u.11132
Ξ±
)
f: Ξ± β†’ β„•
f
) (
ha: a ∈ s
ha
:
a: Ξ±
a
∈
s: Finset Ξ±
s
) : (βˆ‘
i: ?m.11397
i
in
s: Finset Ξ±
s
,
f: Ξ± β†’ β„•
f
i: ?m.11397
i
) /
s: Finset Ξ±
s
.
card: {Ξ± : Type ?u.11411} β†’ Finset Ξ± β†’ β„•
card
≀
f: Ξ± β†’ β„•
f
a: Ξ±
a
:= (
equitableOn_iff_le_le_add_one: βˆ€ {Ξ± : Type ?u.11473} {s : Finset Ξ±} {f : Ξ± β†’ β„•}, EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
equitableOn_iff_le_le_add_one
.
1: βˆ€ {a b : Prop}, (a ↔ b) β†’ a β†’ b
1
h: EquitableOn (↑s) f
h
a: Ξ±
a
ha: a ∈ s
ha
).
1: βˆ€ {a b : Prop}, a ∧ b β†’ a
1
#align finset.equitable_on.le
Finset.EquitableOn.le: βˆ€ {Ξ± : Type u_1} {s : Finset Ξ±} {f : Ξ± β†’ β„•} {a : Ξ±}, EquitableOn (↑s) f β†’ a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a
Finset.EquitableOn.le
theorem
EquitableOn.le_add_one: EquitableOn (↑s) f β†’ a ∈ s β†’ f a ≀ (βˆ‘ i in s, f i) / card s + 1
EquitableOn.le_add_one
(
h: EquitableOn (↑s) f
h
:
EquitableOn: {Ξ± : Type ?u.11527} β†’ {Ξ² : Type ?u.11526} β†’ [inst : LE Ξ²] β†’ [inst : Add Ξ²] β†’ [inst : One Ξ²] β†’ Set Ξ± β†’ (Ξ± β†’ Ξ²) β†’ Prop
EquitableOn
(
s: Finset Ξ±
s
:
Set: Type ?u.11604 β†’ Type ?u.11604
Set
Ξ±: Type ?u.11511
Ξ±
)
f: Ξ± β†’ β„•
f
) (
ha: a ∈ s
ha
:
a: Ξ±
a
∈
s: Finset Ξ±
s
) :
f: Ξ± β†’ β„•
f
a: Ξ±
a
≀ (βˆ‘
i: ?m.11779
i
in
s: Finset Ξ±
s
,
f: Ξ± β†’ β„•
f
i: ?m.11779
i
) /
s: Finset Ξ±
s
.
card: {Ξ± : Type ?u.11793} β†’ Finset Ξ± β†’ β„•
card
+
1: ?m.11798
1
:= (
equitableOn_iff_le_le_add_one: βˆ€ {Ξ± : Type ?u.11915} {s : Finset Ξ±} {f : Ξ± β†’ β„•}, EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1
equitableOn_iff_le_le_add_one
.
1: βˆ€ {a b : Prop}, (a ↔ b) β†’ a β†’ b
1
h: EquitableOn (↑s) f
h
a: Ξ±
a
ha: a ∈ s
ha
).
2: βˆ€ {a b : Prop}, a ∧ b β†’ b
2
#align finset.equitable_on.le_add_one
Finset.EquitableOn.le_add_one: βˆ€ {Ξ± : Type u_1} {s : Finset Ξ±} {f : Ξ± β†’ β„•} {a : Ξ±}, EquitableOn (↑s) f β†’ a ∈ s β†’ f a ≀ (βˆ‘ i in s, f i) / card s + 1
Finset.EquitableOn.le_add_one
theorem
equitableOn_iff: EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ f a = (βˆ‘ i in s, f i) / card s ∨ f a = (βˆ‘ i in s, f i) / card s + 1
equitableOn_iff
:
EquitableOn: {Ξ± : Type ?u.11969} β†’ {Ξ² : Type ?u.11968} β†’ [inst : LE Ξ²] β†’ [inst : Add Ξ²] β†’ [inst : One Ξ²] β†’ Set Ξ± β†’ (Ξ± β†’ Ξ²) β†’ Prop
EquitableOn
(
s: Finset Ξ±
s
:
Set: Type ?u.11976 β†’ Type ?u.11976
Set
Ξ±: Type ?u.11953
Ξ±
)
f: Ξ± β†’ β„•
f
↔ βˆ€
a: ?m.12109
a
∈
s: Finset Ξ±
s
,
f: Ξ± β†’ β„•
f
a: ?m.12109
a
= (βˆ‘
i: ?m.12152
i
in
s: Finset Ξ±
s
,
f: Ξ± β†’ β„•
f
i: ?m.12152
i
) /
s: Finset Ξ±
s
.
card: {Ξ± : Type ?u.12166} β†’ Finset Ξ± β†’ β„•
card
∨
f: Ξ± β†’ β„•
f
a: ?m.12109
a
= (βˆ‘
i: ?m.12236
i
in
s: Finset Ξ±
s
,
f: Ξ± β†’ β„•
f
i: ?m.12236
i
) /
s: Finset Ξ±
s
.
card: {Ξ± : Type ?u.12239} β†’ Finset Ξ± β†’ β„•
card
+
1: ?m.12244
1
:=

Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.11956

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ f a = (βˆ‘ i in s, f i) / card s ∨ f a = (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.11956

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ f a = (βˆ‘ i in s, f i) / card s ∨ f a = (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.11956

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


(βˆ€ (a : Ξ±), a ∈ s β†’ (βˆ‘ i in s, f i) / card s ≀ f a ∧ f a ≀ (βˆ‘ i in s, f i) / card s + 1) ↔ βˆ€ (a : Ξ±), a ∈ s β†’ f a = (βˆ‘ i in s, f i) / card s ∨ f a = (βˆ‘ i in s, f i) / card s + 1
Ξ±: Type u_1

Ξ²: Type ?u.11956

s: Finset Ξ±

f: Ξ± β†’ β„•

a: Ξ±


EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ f a = (βˆ‘ i in s, f i) / card s ∨ f a = (βˆ‘ i in s, f i) / card s + 1

Goals accomplished! πŸ™

Goals accomplished! πŸ™
#align finset.equitable_on_iff
Finset.equitableOn_iff: βˆ€ {Ξ± : Type u_1} {s : Finset Ξ±} {f : Ξ± β†’ β„•}, EquitableOn (↑s) f ↔ βˆ€ (a : Ξ±), a ∈ s β†’ f a = (βˆ‘ i in s, f i) / card s ∨ f a = (βˆ‘ i in s, f i) / card s + 1
Finset.equitableOn_iff
end Finset