MIL/C11_Topology/S01_Filters.lean

GitHub source file

16 declarations, 5 contain sorry, 0 declared as axioms

Imports (2)
Imported by 1 file
  1. def principal sorry line 6 source

    depends on sorry what this means

    Statement uses: Set, Filter

    Proof uses: Filter.mk, setOf, HasSubset.Subset, sorryAx, Lean.Name, Membership.mem, Set.univ, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat, Inter.inter

    4 instances, coercions and auxiliary constants left out.

  2. example (example at line 13) sorry line 13 source
  3. def Tendsto₁ line 19 source

    no axioms what this means

    Statement uses: Filter

    Proof uses: Set, Membership.mem, Set.preimage

    1 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C11_Topology/solutions/Solutions_S01_Filters.lean:29 (same declaration text).

  4. def Tendsto₂ line 22 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Filter

    Proof uses: LE.le, Filter.map

    3 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  5. example (example at line 25) line 25 source
  6. example (example at line 35) sorry line 35 source
  7. example (example at line 52) line 52 source
  8. example (example at line 57) sorry line 57 source
  9. example (example at line 62) line 62 source
  10. example (example at line 65) line 65 source
  11. example (example at line 71) line 71 source
  12. example (example at line 75) line 75 source
  13. example (example at line 79) line 79 source
  14. example (example at line 87) line 87 source
  15. example (example at line 93) line 93 source
  16. example (example at line 102) sorry line 102 source