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
Cmd instead 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 _ }
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 β ] [ Add β ] [ One β ] ( s : Set α ) ( f : α → β ) : Prop :=
∀ ⦃ a₁ a₂ ⦄, a₁ ∈ s → a₂ ∈ s → f a₁ ≤ f a₂ + 1
#align set.equitable_on Set.EquitableOn : {α : Type u_1} → {β : Type u_2} → [inst : LE β [inst : Add β [inst : One β Set α (α → β Prop
@[ simp ]
theorem equitableOn_empty [ LE β ] [ Add β ] [ One β ] ( f : α → β ) : EquitableOn : {α : Type ?u.236} → {β : Type ?u.235} → [inst : LE β [inst : Add β [inst : One β Set α (α → β Prop ∅ f := fun a _ ha =>
( Set.not_mem_empty : ∀ {α : Type ?u.400} (x : α ), ¬ x ∈ ∅ a ha ). elim
#align set.equitable_on_empty 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 α } { f : α → ℕ } :
s . EquitableOn : {α : Type ?u.467} → {β : Type ?u.466} → [inst : LE β [inst : Add β [inst : One β Set α (α → β Prop f ↔ ∃ b , ∀ a ∈ s , b ≤ f a ∧ f a ≤ b + 1 := by
refine' ⟨ _ , fun ⟨ b , hb : ∀ (a : α ), a ∈ s b ≤ f a ∧ f a ≤ b + 1 hb ⟩ x y hx hy => ( hb : ∀ (a : α ), a ∈ s b ≤ f a ∧ f a ≤ b + 1 hb x hx ). 2 : ∀ {a b : Prop }, a ∧ b b . trans : ∀ {α : Type ?u.705} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c trans ( add_le_add_right ( hb : ∀ (a : α ), a ∈ s b ≤ f a ∧ f a ≤ b + 1 hb y hy ). 1 : ∀ {a b : Prop }, a ∧ b a _ )⟩
obtain rfl | ⟨ x , hx ⟩ := s . eq_empty_or_nonempty
· simp
intro hs inr.intro ∃ b , ∀ (a : α ), a ∈ s b ≤ f a ∧ f a ≤ b + 1
by_cases h : ∀ y ∈ s , f x ≤ f y pos ∃ b , ∀ (a : α ), a ∈ s b ≤ f a ∧ f a ≤ b + 1 neg ∃ b , ∀ (a : α ), a ∈ s b ≤ f a ∧ f a ≤ b + 1
· pos ∃ b , ∀ (a : α ), a ∈ s b ≤ f a ∧ f a ≤ b + 1 pos ∃ b , ∀ (a : α ), a ∈ s b ≤ f a ∧ f a ≤ b + 1 neg ∃ b , ∀ (a : α ), a ∈ s b ≤ f a ∧ f a ≤ b + 1 exact ⟨ f x , fun y hy => ⟨ h _ hy , hs hy hx ⟩⟩
push_neg at h neg ∃ b , ∀ (a : α ), a ∈ s b ≤ f a ∧ f a ≤ b + 1
obtain ⟨w, hw, hwx⟩ : w ∈ s ∧ f w < f x w ⟨w, hw, hwx⟩ : w ∈ s ∧ f w < f x hw ⟨w, hw, hwx⟩ : w ∈ s ∧ f w < f x hwx ⟨w, hw, hwx⟩ : w ∈ s ∧ f w < f x := h : ∃ y , y ∈ s ∧ f y < f x h neg.intro.intro ∃ b , ∀ (a : α ), a ∈ s b ≤ f a ∧ f a ≤ b + 1
refine' ⟨ f w , fun y hy => ⟨ Nat.le_of_succ_le_succ _ , hs hy hw ⟩⟩
rw [ ( Nat.succ_le_of_lt hwx ). antisymm ( hs hx hw ) ]
exact hs hx hy
#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
theorem equitableOn_iff_exists_image_subset_icc { s : Set α } { f : α → ℕ } :
s . EquitableOn : {α : Type ?u.4654} → {β : Type ?u.4653} → [inst : LE β [inst : Add β [inst : One β Set α (α → β Prop f ↔ ∃ b , f '' s ⊆ Icc b ( b + 1 ) := by
simpa only [ image_subset_iff : ∀ {α : Type ?u.4931} {β : Type ?u.4932} {s : Set α t : Set β f : α → β f '' s ⊆ t ↔ s ⊆ f ⁻¹' t ] using equitableOn_iff_exists_le_le_add_one : ∀ {α : Type ?u.5236} {s : Set α f : α → ℕ EquitableOn s f ↔ ∃ b , ∀ (a : α ), a ∈ s b ≤ f a ∧ f a ≤ b + 1
#align set.equitable_on_iff_exists_image_subset_Icc 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 α } { f : α → ℕ } :
s . EquitableOn : {α : Type ?u.5357} → {β : Type ?u.5356} → [inst : LE β [inst : Add β [inst : One β Set α (α → β Prop f ↔ ∃ b , ∀ a ∈ s , f a = b ∨ f a = b + 1 := by
simp_rw [ equitableOn_iff_exists_le_le_add_one : ∀ {α : Type ?u.5668} {s : Set α f : α → ℕ EquitableOn s f ↔ ∃ b , ∀ (a : α ), a ∈ s b ≤ f a ∧ f a ≤ b + 1 , (∃ b , ∀ (a : α ), a ∈ s b ≤ f a ∧ f a ≤ b + 1 ) ↔ ∃ b , ∀ (a : α ), a ∈ s f a = b ∨ f a = b + 1 Nat.le_and_le_add_one_iff ]
#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
section OrderedSemiring
variable [ OrderedSemiring : Type ?u.6182 → Type ?u.6182 β ]
theorem Subsingleton.equitableOn { s : Set α } ( hs : s . Subsingleton ) ( f : α → β ) : s . EquitableOn : {α : Type ?u.6200} → {β : Type ?u.6199} → [inst : LE β [inst : Add β [inst : One β Set α (α → β Prop f :=
fun i j hi hj => by
rw [ hs hi hj ]
exact le_add_of_nonneg_right : ∀ {α : Type ?u.6780} [inst : AddZeroClass α inst_1 : LE α inst_2 : CovariantClass α α (fun x x_1 => x + x_1 ) fun x x_1 => x ≤ x_1 a b : α }, 0 ≤ b a ≤ a + b zero_le_one
#align set.subsingleton.equitable_on Set.Subsingleton.equitableOn
theorem equitableOn_singleton ( a : α ) ( f : α → β ) : Set.EquitableOn : {α : Type ?u.7745} → {β : Type ?u.7744} → [inst : LE β [inst : Add β [inst : One β Set α (α → β Prop { a } f :=
Set.subsingleton_singleton . equitableOn f
#align set.equitable_on_singleton Set.equitableOn_singleton
end OrderedSemiring
end Set
open Set
namespace Finset
variable { s : Finset α } { f : α → ℕ } { a : α }
theorem equitableOn_iff_le_le_add_one :
EquitableOn : {α : Type ?u.8334} → {β : Type ?u.8333} → [inst : LE β [inst : Add β [inst : One β Set α (α → β Prop ( s : Set α ) f ↔
∀ a ∈ s , (∑ i in s , f i ) / s . card ≤ f a ∧ f a ≤ (∑ i in s , f i ) / s . card + 1 := by
rw [ Set.equitableOn_iff_exists_le_le_add_one : ∀ {α : Type ?u.8703} {s : Set α f : α → ℕ EquitableOn s f ↔ ∃ b , ∀ (a : α ), a ∈ s b ≤ f a ∧ f a ≤ b + 1 (∃ 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 ] (∃ 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
refine' ⟨ _ , fun h => ⟨ _ , h ⟩⟩ (∃ 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
rintro ⟨ b , hb : ∀ (a : α ), a ∈ ↑s b ≤ f a ∧ f a ≤ b + 1 hb ⟩ intro ∀ (a : α ), a ∈ s (∑ i in s , f i ) / card s ≤ f a ∧ f a ≤ (∑ i in s , f i ) / card s + 1
by_cases h : ∀ a ∈ s , f a = b + 1 α : Type u_1β : Type ?u.8321s : 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.8321s : 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.8321s : 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.8321s : 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.8321s : 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 intro a ha α : Type u_1β : Type ?u.8321s : 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
α : Type u_1β : Type ?u.8321s : 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 rw [ α : Type u_1β : Type ?u.8321s : 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 h _ ha , α : Type u_1β : Type ?u.8321s : 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 α : Type u_1β : Type ?u.8321s : 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 sum_const_nat : ∀ {α : Type ?u.9509} {s : Finset α m : ℕ } {f : α → ℕ (∀ (x : α ), x ∈ s f x = m ) → ∑ x in s , f x = card s * m h , α : Type u_1β : Type ?u.8321s : 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 α : Type u_1β : Type ?u.8321s : 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 Nat.mul_div_cancel_left : ∀ (m : ℕ ) {n : ℕ }, 0 < n n * m / n = m _ ( card_pos . 2 : ∀ {a b : Prop }, (a ↔ b b → a ⟨ a , ha ⟩) α : Type u_1β : Type ?u.8321s : 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 ] α : Type u_1β : Type ?u.8321s : 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
α : Type u_1β : Type ?u.8321s : 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 exact ⟨ le_rfl , Nat.le_succ _ ⟩
push_neg at h α : Type u_1β : Type ?u.8321s : 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
obtain ⟨x, hx₁, hx₂⟩ : x ∈ s ∧ f x ≠ b + 1 x ⟨x, hx₁, hx₂⟩ : x ∈ s ∧ f x ≠ b + 1 hx₁ ⟨x, hx₁, hx₂⟩ : x ∈ s ∧ f x ≠ b + 1 hx₂ ⟨x, hx₁, hx₂⟩ : x ∈ s ∧ f x ≠ b + 1 := h : ∃ a , a ∈ s ∧ f a ≠ b + 1 h α : Type u_1β : Type ?u.8321s : 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
suffices h : b = (∑ i in s , f i ) / card s h : b = (∑ i in s , f i ) / s . card α : Type u_1β : Type ?u.8321s : 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.8321s : 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
· α : Type u_1β : Type ?u.8321s : 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.8321s : 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.8321s : 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 simp_rw [ α : Type u_1β : Type ?u.8321s : 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 ← h : b = (∑ i in s , f i ) / card s h α : Type u_1β : Type ?u.8321s : 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.8321s : 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.8321s : 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 apply hb : ∀ (a : α ), a ∈ ↑s b ≤ f a ∧ f a ≤ b + 1 hb
symm α : Type u_1β : Type ?u.8321s : 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
refine'
Nat.div_eq_of_lt_le : ∀ {k n m : ℕ }, k * n ≤ m m < Nat.succ k * n m / n = k ( le_trans : ∀ {α : Type ?u.10145} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c ( α : Type u_1β : Type ?u.8321s : 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 by α : Type u_1β : Type ?u.8321s : Finset α f : α → ℕ a : α b : ℕ hb : ∀ (a : α ), a ∈ ↑s b ≤ f a ∧ f a ≤ b + 1 x : α hx₁ : x ∈ s hx₂ : f x ≠ b + 1 simp [ mul_comm ] ) ( sum_le_sum fun a ha => ( hb : ∀ (a : α ), a ∈ ↑s b ≤ f a ∧ f a ≤ b + 1 hb a ha ). 1 : ∀ {a b : Prop }, a ∧ b a ))
(( sum_lt_sum ( fun a ha => ( hb : ∀ (a : α ), a ∈ ↑s b ≤ f a ∧ f a ≤ b + 1 hb a ha ). 2 : ∀ {a b : Prop }, a ∧ b b ) ⟨ _ , hx₁ , ( hb : ∀ (a : α ), a ∈ ↑s b ≤ f a ∧ f a ≤ b + 1 hb _ hx₁ ). 2 : ∀ {a b : Prop }, a ∧ b b . lt_of_ne hx₂ ⟩). trans_le : ∀ {α : Type ?u.10384} [inst : Preorder α a b c : α }, a < b b ≤ c a < c trans_le _ ) α : Type u_1β : Type ?u.8321s : 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
rw [ α : Type u_1β : Type ?u.8321s : 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 mul_comm , α : Type u_1β : Type ?u.8321s : 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 α : Type u_1β : Type ?u.8321s : 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 sum_const_nat : ∀ {α : Type ?u.11009} {s : Finset α m : ℕ } {f : α → ℕ (∀ (x : α ), x ∈ s f x = m ) → ∑ x in s , f x = card s * m α : Type u_1β : Type ?u.8321s : 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 α : Type u_1β : Type ?u.8321s : 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.8321s : 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.8321s : 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
exact fun _ _ => rfl : ∀ {α : Sort ?u.11043} {a : α }, a = a
#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
theorem EquitableOn.le ( h : EquitableOn : {α : Type ?u.11148} → {β : Type ?u.11147} → [inst : LE β [inst : Add β [inst : One β Set α (α → β Prop ( s : Set α ) f ) ( ha : a ∈ s ) :
(∑ i in s , f i ) / s . card ≤ f a :=
( equitableOn_iff_le_le_add_one . 1 : ∀ {a b : Prop }, (a ↔ b a → b h a ha ). 1 : ∀ {a b : Prop }, a ∧ b a
#align finset.equitable_on.le Finset.EquitableOn.le
theorem EquitableOn.le_add_one ( h : EquitableOn : {α : Type ?u.11527} → {β : Type ?u.11526} → [inst : LE β [inst : Add β [inst : One β Set α (α → β Prop ( s : Set α ) f ) ( ha : a ∈ s ) :
f a ≤ (∑ i in s , f i ) / s . card + 1 :=
( equitableOn_iff_le_le_add_one . 1 : ∀ {a b : Prop }, (a ↔ b a → b h a ha ). 2 : ∀ {a b : Prop }, a ∧ b b
#align finset.equitable_on.le_add_one Finset.EquitableOn.le_add_one
theorem equitableOn_iff :
EquitableOn : {α : Type ?u.11969} → {β : Type ?u.11968} → [inst : LE β [inst : Add β [inst : One β Set α (α → β Prop ( s : Set α ) f ↔
∀ a ∈ s , f a = (∑ i in s , f i ) / s . card ∨ f a = (∑ i in s , f i ) / s . card + 1 :=
by simp_rw [ equitableOn_iff_le_le_add_one , (∀ (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 Nat.le_and_le_add_one_iff ]
#align finset.equitable_on_iff Finset.equitableOn_iff
end Finset