Carleson/MinLayerTiles.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
Imported by 2 files
  1. lemma exists_scale_add_le_of_mem_minLayer line 16 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Membership.mem, Set.minLayer, Exists, And and 4 more

    Proof uses: Nat.recAux, Exists.intro, And.intro, le_rfl, Set.exists_le_in_minLayer_of_le, LE.le.trans, LT.lt, Grid, π“˜, π“˜_strictMono, lt_of_le_of_ne, Disjoint.ne_of_mem, Set.disjoint_minLayer_of_ne, And.right, s, Eq.mp, congrArg, propext, Grid.lt_def

    56 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

  2. lemma exists_le_add_scale_of_mem_maxLayer line 28 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Membership.mem, Set.maxLayer, Exists, And and 4 more

    Proof uses: Nat.recAux, Exists.intro, And.intro, le_rfl, Set.exists_le_in_maxLayer_of_le, LE.le.trans, LT.lt, Grid, π“˜, π“˜_strictMono, lt_of_le_of_ne, Disjoint.ne_of_mem, Set.disjoint_maxLayer_of_ne, And.right, s, Eq.mp, congrArg, propext, Grid.lt_def

    56 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

  3. lemma exists_scale_add_le_of_mem_layersAbove line 40 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Membership.mem, Set.layersAbove, Exists, And and 5 more

    Proof uses: Set.exists_le_in_layersAbove_of_le, le_rfl, exists_scale_add_le_of_mem_minLayer, Exists.intro, And.intro, LE.le.trans, And.right, Prod.fst, GridStructure.Grid, Prod.mk, GridStructure.s, Grid, OrderDual, FunctionDistances.Θ, toTileLike, Prod.snd, And.left

    65 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  4. lemma exists_le_add_scale_of_mem_layersBelow line 46 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Membership.mem, Set.layersBelow, Exists, And and 5 more

    Proof uses: Set.exists_le_in_layersBelow_of_le, le_rfl, exists_le_add_scale_of_mem_maxLayer, Exists.intro, And.intro, LE.le.trans, Prod.snd, GridStructure.Grid, Prod.mk, GridStructure.s, Prod.fst, Grid, OrderDual, FunctionDistances.Θ, toTileLike, add_le_add_left, And.right, And.left

    68 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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