𝕜 : Type ?u.28107
ι : Type ?u.28110
κ : Type ?u.28113
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
hst : ↑(card s₂) * ↑(card t₂) ≠ 0
⊢ ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁)) * edgeDensity r s₂ t₂ ≤ edgeDensity r s₁ t₁
𝕜 : Type ?u.28107
ι : Type ?u.28110
κ : Type ?u.28113
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁)) * edgeDensity r s₂ t₂ ≤ edgeDensity r s₁ t₁
have hst : (s₂.card : ℚ) * t₂.card ≠ 0 := by simp [hs₂.ne_empty, ht₂.ne_empty]
𝕜 : Type ?u.28107
ι : Type ?u.28110
κ : Type ?u.28113
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
hst : ↑(card s₂) * ↑(card t₂) ≠ 0
⊢ ↑(card (interedges r s₂ t₂)) / (↑(card s₁) * ↑(card t₁)) ≤ ↑(card (interedges r s₁ t₁)) / (↑(card s₁) * ↑(card t₁))
𝕜 : Type ?u.28107
ι : Type ?u.28110
κ : Type ?u.28113
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
hst : ↑(card s₂) * ↑(card t₂) ≠ 0
⊢ ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁)) * edgeDensity r s₂ t₂ ≤ edgeDensity r s₁ t₁
rw [edgeDensity, edgeDensity, div_mul_div_comm, mul_comm, div_mul_div_cancel _ hst]
𝕜 : Type ?u.28107
ι : Type ?u.28110
κ : Type ?u.28113
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
hst : ↑(card s₂) * ↑(card t₂) ≠ 0
⊢ ↑(card (interedges r s₂ t₂)) ≤ ↑(card (interedges r s₁ t₁))
𝕜 : Type ?u.28107
ι : Type ?u.28110
κ : Type ?u.28113
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
hst : ↑(card s₂) * ↑(card t₂) ≠ 0
⊢ ↑(card (interedges r s₂ t₂)) / (↑(card s₁) * ↑(card t₁)) ≤ ↑(card (interedges r s₁ t₁)) / (↑(card s₁) * ↑(card t₁))
refine' div_le_div_of_le (by exact_mod_cast (s₁.card * t₁.card).zero_le) _
no goals
𝕜 : Type ?u.28107
ι : Type ?u.28110
κ : Type ?u.28113
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
hst : ↑(card s₂) * ↑(card t₂) ≠ 0
⊢ ↑(card (interedges r s₂ t₂)) ≤ ↑(card (interedges r s₁ t₁))
exact_mod_cast card_le_of_subset (interedges_mono hs ht)
no goals
𝕜 : Type ?u.28107
ι : Type ?u.28110
κ : Type ?u.28113
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ ↑(card s₂) * ↑(card t₂) ≠ 0
simp [hs₂.ne_empty, ht₂.ne_empty]
no goals
𝕜 : Type ?u.28107
ι : Type ?u.28110
κ : Type ?u.28113
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
hst : ↑(card s₂) * ↑(card t₂) ≠ 0
⊢ 0 ≤ ↑(card s₁) * ↑(card t₁)
exact_mod_cast (s₁.card * t₁.card).zero_le