English
If a bound 100 ≤ 4^k · ε^5 holds, then ε^5 > 0.
Русский
Если верно 100 ≤ 4^k · ε^5, то ε^5 > 0.
LaTeX
$$$100 \\le 4^k \\cdot ε^5 \\Rightarrow ε^5 > 0$$$
Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.HSub.hSub]
public meta def
_aux_Mathlib_Combinatorics_SimpleGraph_Regularity_Bound___delab_app__private_Mathlib_Combinatorics_SimpleGraph_Regularity_Bound_0_termA_1 :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 6
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `HSub.hSub)) (matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `HDiv.hDiv))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
pure✝)
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Fintype.card))
(matchFVar✝ `α (matchExpr✝ isType'✝)))
pure✝))
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset.card))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset)) (matchFVar✝ `α (matchExpr✝ isType'✝))))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finpartition.parts))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset))
(matchFVar✝ `α (matchExpr✝ isType'✝))))
pure✝)
pure✝)
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset.univ))
(matchFVar✝ `α (matchExpr✝ isType'✝)))
pure✝))
(matchFVar✝ `P
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finpartition))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset))
(matchFVar✝ `α (matchExpr✝ isType'✝))))
pure✝)
pure✝)
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset.univ))
(matchFVar✝ `α (matchExpr✝ isType'✝)))
pure✝)))))))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `HMul.hMul))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `HDiv.hDiv))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
pure✝)
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Fintype.card))
(matchFVar✝ `α (matchExpr✝ isType'✝)))
pure✝))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `SzemerediRegularity.stepBound))
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset.card))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset))
(matchFVar✝ `α (matchExpr✝ isType'✝))))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finpartition.parts))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset))
(matchFVar✝ `α (matchExpr✝ isType'✝))))
pure✝)
pure✝)
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset.univ))
(matchFVar✝ `α (matchExpr✝ isType'✝)))
pure✝))
(matchFVar✝ `P
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finpartition))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset))
(matchFVar✝ `α (matchExpr✝ isType'✝))))
pure✝)
pure✝)
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset.univ))
(matchFVar✝ `α (matchExpr✝ isType'✝)))
pure✝))))))))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `HPow.hPow))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(natLitMatcher✝ 4))
pure✝))
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset.card))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset)) (matchFVar✝ `α (matchExpr✝ isType'✝))))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finpartition.parts))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset))
(matchFVar✝ `α (matchExpr✝ isType'✝))))
pure✝)
pure✝)
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset.univ))
(matchFVar✝ `α (matchExpr✝ isType'✝)))
pure✝))
(matchFVar✝ `P
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finpartition))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset))
(matchFVar✝ `α (matchExpr✝ isType'✝))))
pure✝)
pure✝)
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset.univ))
(matchFVar✝ `α (matchExpr✝ isType'✝)))
pure✝))))))) >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => withHeadRefIfTagAppFns✝ `(a))
