Theorems · Theorem · general topology

Filter.CountableFilterBasis.mk.inj

∀ {α : Type u_6} {toFilterBasis : FilterBasis α} {countable : toFilterBasis.sets.Countable}
  {toFilterBasis_1 : FilterBasis α} {countable_1 : toFilterBasis_1.sets.Countable},
  { toFilterBasis := toFilterBasis, countable := countable } =
      { toFilterBasis := toFilterBasis_1, countable := countable_1 } →
    toFilterBasis = toFilterBasis_1

Defined in

Mathlib.Order.Filter.CountablyGenerated

Cited by

1 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms