Pi

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

Statistics

Metric	Count
Definitions coprodᵢ	1
Theorems eval_pi, pi_self, coprodᵢ, neBot, apply, pi_map_coprodᵢ, compl_mem_coprodᵢ, coprodᵢ_bot, coprodᵢ_bot', coprodᵢ_eq_bot_iff, coprodᵢ_eq_bot_iff', coprodᵢ_mono, coprodᵢ_neBot, coprodᵢ_neBot_iff, coprodᵢ_neBot_iff', eventually_pi, hasBasis_pi, hasBasis_pi_principal, hasBasis_pi_pure, hasBasis_pi_same_index, instNeBotForallPi, le_pi, le_pi_principal, map_eval_pi, map_pi_map_coprodᵢ_le, mem_coprodᵢ_iff, mem_of_pi_mem_pi, mem_pi, mem_pi', mem_pi_of_mem, mem_pi_principal, mem_pi_pure, pi_comap, pi_eq_bot, pi_inf_principal_pi_eq_bot, pi_inf_principal_pi_neBot, pi_inf_principal_univ_pi_eq_bot, pi_inf_principal_univ_pi_neBot, pi_inj, pi_le_pi, pi_mem_pi, pi_mem_pi_iff, pi_mono, pi_neBot, pi_principal, pi_pure, tendsto_eval_pi, tendsto_pi, tendsto_piMap_pi	49
Total	50

Filter

Definitions

Name	Category	Theorems
coprodᵢ 📖	CompOp	16 math math: coprodᵢ_cocompact, coprodᵢ_mono, compl_mem_coprodᵢ, mem_coprodᵢ_iff, coprodᵢ_neBot_iff, map_pi_map_coprodᵢ_le, coprodᵢ_bot, coprodᵢ_eq_bot_iff, coprodᵢ_bot', NeBot.coprodᵢ, coprodᵢ_cofinite, coprodᵢ_eq_bot_iff', coprodᵢ_neBot, coprodᵢ_neBot_iff', Bornology.cobounded_pi, Tendsto.pi_map_coprodᵢ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl_mem_coprodᵢ 📖	mathematical	—	Set Filter instMembership coprodᵢ Compl.compl Set.instCompl Set.image Function.eval	—	—
coprodᵢ_bot 📖	mathematical	—	coprodᵢ Bot.bot Filter instBot	—	coprodᵢ_bot'
coprodᵢ_bot' 📖	mathematical	—	coprodᵢ Bot.bot Pi.instBotForall Filter instBot	—	coprodᵢ_eq_bot_iff'
coprodᵢ_eq_bot_iff 📖	mathematical	—	coprodᵢ Bot.bot Filter instBot Pi.instBotForall	—	Iff.not coprodᵢ_neBot_iff
coprodᵢ_eq_bot_iff' 📖	mathematical	—	coprodᵢ Bot.bot Filter instBot IsEmpty Pi.instBotForall	—	Iff.not coprodᵢ_neBot_iff'
coprodᵢ_mono 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder	coprodᵢ	—	iSup_mono comap_mono
coprodᵢ_neBot 📖	mathematical	NeBot	coprodᵢ	—	NeBot.coprodᵢ
coprodᵢ_neBot_iff 📖	mathematical	—	NeBot coprodᵢ	—	—
coprodᵢ_neBot_iff' 📖	mathematical	—	NeBot coprodᵢ	—	—
eventually_pi 📖	mathematical	Eventually	pi	—	eventually_all Eventually.eval_pi
hasBasis_pi 📖	mathematical	HasBasis	Set pi Set.Finite Set.pi	—	Set.pi_def HasBasis.iInf' HasBasis.comap
hasBasis_pi_principal 📖	mathematical	—	HasBasis Set pi principal Set.Finite Set.pi	—	mem_pi_principal
hasBasis_pi_pure 📖	mathematical	—	HasBasis Set pi Filter instPure Set.Finite setOf	—	mem_pi_pure
hasBasis_pi_same_index 📖	mathematical	HasBasis Set Set.instHasSubset	pi Set.Finite Set.pi	—	HasBasis.to_hasBasis hasBasis_pi Set.pi_mono subset_rfl Set.instReflSubset
instNeBotForallPi 📖	mathematical	NeBot	pi	—	pi_neBot
le_pi 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder pi Tendsto Function.eval	—	tendsto_pi
le_pi_principal 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder principal Set.pi Set.univ pi	—	le_pi tendsto_principal_principal
map_eval_pi 📖	mathematical	NeBot	map Function.eval pi	—	le_antisymm tendsto_eval_pi mem_pi mem_map mem_of_superset HasSubset.Subset.trans Set.instIsTransSubset Set.subset_eval_image_pi nonempty_of_mem instNeBotForallPi pi_mem_pi Set.image_subset_iff
map_pi_map_coprodᵢ_le 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder map coprodᵢ	—	—
mem_coprodᵢ_iff 📖	mathematical	—	Set Filter instMembership coprodᵢ Set.instHasSubset Set.preimage Function.eval	—	—
mem_of_pi_mem_pi 📖	—	NeBot Set Filter instMembership pi Set.pi Set.instMembership	—	—	mem_pi mem_of_superset nonempty_of_mem eq_or_ne Function.update_self Function.update_of_ne
mem_pi 📖	mathematical	—	Set Filter instMembership pi Set.Finite Set.instHasSubset Set.pi	—	Set.pi_def Set.iInter₂_mono mem_of_superset pi_mem_pi
mem_pi' 📖	mathematical	—	Set Filter instMembership pi Set.instHasSubset Set.pi SetLike.coe Finset Finset.instSetLike	—	mem_pi Set.exists_finite_iff_finset
mem_pi_of_mem 📖	mathematical	Set Filter instMembership	pi Set.preimage Function.eval	—	mem_iInf_of_mem preimage_mem_comap
mem_pi_principal 📖	mathematical	—	Set Filter instMembership pi principal Set.Finite Set.instHasSubset Set.pi	—	HasBasis.mem_iff hasBasis_pi hasBasis_principal
mem_pi_pure 📖	mathematical	—	Set Filter instMembership pi instPure Set.Finite Set.instMembership	—	—
pi_comap 📖	mathematical	—	pi comap Pi.map	—	comap_comap comap_iInf
pi_eq_bot 📖	mathematical	—	pi Bot.bot Filter instBot	—	Set.pi_univ principal_univ inf_of_le_left pi_inf_principal_univ_pi_eq_bot
pi_inf_principal_pi_eq_bot 📖	mathematical	NeBot	Filter instInf pi principal Set.pi Bot.bot instBot Set Set.instMembership	—	Set.univ_pi_piecewise_univ pi_inf_principal_univ_pi_eq_bot Set.piecewise_eq_of_mem Set.piecewise_eq_of_notMem principal_univ inf_of_le_left
pi_inf_principal_pi_neBot 📖	mathematical	NeBot	Filter instInf pi principal Set.pi	—	—
pi_inf_principal_univ_pi_eq_bot 📖	mathematical	—	Filter instInf pi principal Set.pi Set.univ Bot.bot instBot	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq Frequently.exists Frequently.and_eventually Set.mem_univ_pi mp_mem mem_pi_of_mem univ_mem'
pi_inf_principal_univ_pi_neBot 📖	mathematical	—	NeBot Filter instInf pi principal Set.pi Set.univ	—	—
pi_inj 📖	mathematical	NeBot	pi	—	pi_le_pi Eq.le LE.le.antisymm neBot_of_le Eq.ge
pi_le_pi 📖	mathematical	NeBot	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder pi	—	Tendsto.mono_left tendsto_eval_pi map_eval_pi pi_mono
pi_mem_pi 📖	mathematical	Set Filter instMembership	pi Set.pi	—	Set.pi_def Set.biInter_eq_iInter mem_iInf_of_iInter preimage_mem_comap Set.Subset.rfl
pi_mem_pi_iff 📖	mathematical	NeBot	Set Filter instMembership pi Set.pi	—	mem_of_pi_mem_pi pi_mem_pi
pi_mono 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder	pi	—	iInf_mono comap_mono
pi_neBot 📖	mathematical	—	NeBot pi	—	—
pi_principal 📖	mathematical	—	pi principal Set.pi Set.univ	—	comap_principal iInf_principal' Set.pi_def Set.iInter_congr_Prop Set.iInter_true
pi_pure 📖	mathematical	—	pi Filter instPure	—	pi_principal Set.univ_pi_singleton
tendsto_eval_pi 📖	mathematical	—	Tendsto Function.eval pi	—	tendsto_iInf' tendsto_comap
tendsto_pi 📖	mathematical	—	Tendsto pi	—	—
tendsto_piMap_pi 📖	mathematical	Tendsto	Pi.map pi	—	tendsto_pi Tendsto.comp tendsto_eval_pi

Filter.Eventually

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eval_pi 📖	mathematical	Filter.Eventually	Filter.pi	—	Filter.Tendsto.eventually Filter.tendsto_eval_pi

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi_self 📖	mathematical	Filter.HasBasis	Set Filter.pi Set.Finite Set.pi	—	Filter.hasBasis_pi_same_index mem_iff Filter.biInter_mem mem_of_mem HasSubset.Subset.trans Set.instIsTransSubset Set.biInter_subset_of_mem

Filter.NeBot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coprodᵢ 📖	mathematical	—	Filter.NeBot Filter.coprodᵢ	—	Filter.coprodᵢ_neBot_iff

Filter.PiInfPrincipalPi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
neBot 📖	mathematical	Filter.NeBot Filter Filter.instInf Filter.principal	Filter.pi Set.pi	—	Filter.NeBot.mono Filter.pi_inf_principal_univ_pi_neBot inf_le_inf_left Filter.principal_mono

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply 📖	—	Filter.Tendsto Filter.pi	—	—	Filter.tendsto_pi
pi_map_coprodᵢ 📖	mathematical	Filter.Tendsto	Filter.coprodᵢ	—	LE.le.trans Filter.map_pi_map_coprodᵢ_le Filter.coprodᵢ_mono

---

← Back to Index