Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_Mathlib_Order_Filter_Cofinite.lean

definition moduleadapted from the Imperial College London FLT project: FLT/Mathlib/Order/Filter/Cofinite.lean

Countability of the cofinite filter's sets on a countable type

Two general facts about the cofinite filter are recorded for an arbitrary countable index type \iota. The lemma Filter.cofinite.sets.countable asserts that the collection of members of Filter.cofinite on \iota — that is, the family of subsets s \subseteq \iota whose complement s^{c} is finite, viewed as a subset of the power set of \iota — is a countable set in the sense of Set.Countable. The proof rests on the fact that the finite subsets of a countable type form a countable family together with the involution s \mapsto s^{c} on subsets of \iota, which is a bijection and hence injective on any set; the cofinite sets are exactly the preimage of the finite sets under this involution.

The accompanying instance packages the same statement in type-theoretic form: for a countable type \iota, the subtype of subsets of \iota belonging to Filter.cofinite, regarded as a type via the coercion of its set of members, carries a Countable instance. The two formulations are interchanged through the equivalence between countability of a set and countability of its associated subtype.

Relation to Mathlib

Filter.cofinite, Set.Countable and compl_bijective are Mathlib notions; this module only adds the countability statement for the members of the cofinite filter on a countable type, in both its set-level and its typeclass form.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_Mathlib_Order_Filter_Cofinite.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

section

lemma Filter.cofinite.sets.countable (ι : Type*) [Countable ι] :
    (Filter.cofinite : Filter ι).sets.Countable :=
  Set.Countable.mono (fun _ h ↦ h) <|
  Set.Countable.preimage_of_injOn Set.Countable.setOf_finite compl_bijective.1.injOn

instance (ι : Type*) [Countable ι] : Countable (.cofinite : Filter ι).sets := by
  rw [Set.countable_coe_iff]
  exact Filter.cofinite.sets.countable ι

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).