FormalConjectures/Mathoverflow/347178.lean

GitHub source file

3 declarations, 3 contain sorry, 0 declared as axioms

Mathoverflow 347178

Reference: mathoverflow/347178 asked by user Biagio Ricceri

Imports (1)
  1. theorem Mathoverflow347178.mathoverflow_347178 sorry line 43 source

    depends on sorry what this means

    Statement uses: Iff, False, Nat, GE.ge, OfNat.ofNat, EuclideanSpace, Real, Fin, ContDiff, ENNReal, WithTop, ENat, And, BddAbove, Set.range, HAdd.hAdd, gradient, Eq, EReal, iSup

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    90 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  2. theorem Mathoverflow347178.mathoverflow_347178.variants.bounded_iff sorry line 58 source

    depends on sorry what this means

    Statement uses: Iff, False, Nat, GE.ge, OfNat.ofNat, EuclideanSpace, Real, Fin, ContDiff, ENNReal, WithTop, ENat, BddAbove, Set.range, HAdd.hAdd, gradient

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    86 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  3. theorem Mathoverflow347178.mathoverflow_347178.variants.bounded_only sorry line 73 source

    depends on sorry what this means

    Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, EuclideanSpace, Real, Fin, ContDiff, ENNReal, WithTop, ENat, BddAbove, Set.range, HAdd.hAdd, gradient, Eq, iSup

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    88 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.