Documentation Verification Report

Ker

📁 Source: Mathlib/Order/Filter/Ker.lean

Statistics

Metric	Count
Definitions `gi_principal_ker`	1
Theorems `ker_bot`, `ker_comap`, `ker_def`, `ker_eq_univ`, `ker_iInf`, `ker_iSup`, `ker_inf`, `ker_mono`, `ker_pi`, `ker_principal`, `ker_prod`, `ker_pure`, `ker_sInf`, `ker_sSup`, `ker_sup`, `ker_surjective`, `ker_top`, `mem_ker`, `subset_ker`	19
Total	20

Filter

Definitions

Name	Category	Theorems
`gi_principal_ker` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ker_bot` 📖	mathematical	—	`ker` `Bot.bot` `Filter` `instBot` `Set` `Set.instEmptyCollection`	—	`Set.sInter_eq_empty_iff`
`ker_comap` 📖	mathematical	—	`ker` `comap` `Set.preimage`	—	`Set.ext` `forall_swap` `Set.Subset.rfl`
`ker_def` 📖	mathematical	—	`ker` `Set.iInter` `Set` `Filter` `instMembership`	—	`Set.sInter_eq_biInter`
`ker_eq_univ` 📖	mathematical	—	`ker` `Set.univ` `Top.top` `Filter` `instTop`	—	`GaloisConnection.u_eq_top` `GaloisCoinsertion.gc` `principal_univ`
`ker_iInf` 📖	mathematical	—	`ker` `iInf` `Filter` `instInfSet` `Set.iInter`	—	`GaloisConnection.u_iInf` `GaloisCoinsertion.gc`
`ker_iSup` 📖	mathematical	—	`ker` `iSup` `Filter` `instSupSet` `Set.iUnion`	—	`subset_antisymm` `Set.instAntisymmSubset` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `mem_iSup` `mem_of_superset` `Set.subset_iUnion` `Monotone.le_map_iSup` `ker_mono`
`ker_inf` 📖	mathematical	—	`ker` `Filter` `instInf` `Set` `Set.instInter`	—	`GaloisConnection.u_inf` `GaloisCoinsertion.gc`
`ker_mono` 📖	mathematical	—	`Monotone` `Filter` `Set` `PartialOrder.toPreorder` `instPartialOrder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ker`	—	`GaloisConnection.monotone_u` `GaloisCoinsertion.gc`
`ker_pi` 📖	mathematical	—	`ker` `pi` `Set.pi` `Set.univ`	—	`ker_iInf` `ker_comap` `Set.pi_def` `Set.iInter_congr_Prop` `Set.iInter_true`
`ker_principal` 📖	mathematical	—	`ker` `principal`	—	`GaloisCoinsertion.u_l_eq`
`ker_prod` 📖	mathematical	—	`ker` `SProd.sprod` `Filter` `instSProd` `Set` `Set.instSProd`	—	`ker_inf` `ker_comap`
`ker_pure` 📖	mathematical	—	`ker` `Filter` `instPure` `Set` `Set.instSingletonSet`	—	`principal_singleton` `ker_principal`
`ker_sInf` 📖	mathematical	—	`ker` `InfSet.sInf` `Filter` `instInfSet` `Set.iInter` `Set` `Set.instMembership`	—	`GaloisConnection.u_sInf` `GaloisCoinsertion.gc`
`ker_sSup` 📖	mathematical	—	`ker` `SupSet.sSup` `Filter` `instSupSet` `Set.iUnion` `Set` `Set.instMembership`	—	`sSup_eq_iSup` `ker_iSup`
`ker_sup` 📖	mathematical	—	`ker` `Filter` `instSup` `Set` `Set.instUnion`	—	`sSup_pair` `ker_sSup` `Set.biUnion_pair`
`ker_surjective` 📖	mathematical	—	`Filter` `Set` `ker`	—	`GaloisCoinsertion.u_surjective`
`ker_top` 📖	mathematical	—	`ker` `Top.top` `Filter` `instTop` `Set.univ`	—	`GaloisConnection.u_top` `GaloisCoinsertion.gc`
`mem_ker` 📖	mathematical	—	`Set` `Set.instMembership` `ker`	—	`Set.mem_sInter`
`subset_ker` 📖	mathematical	—	`Set` `Set.instHasSubset` `ker`	—	`Set.subset_sInter_iff`

---

← Back to Index