Lift

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

Statistics

Metric	Count
Definitions	0
Theorems lift', mem_lift_iff, comap_eq_lift', comap_lift'_eq, comap_lift'_eq2, comap_lift_eq, comap_lift_eq2, eventually_lift'_iff, le_lift, le_lift', lift'_bot, lift'_cong, lift'_iInf, lift'_iInf_of_map_univ, lift'_id, lift'_inf, lift'_inf_le, lift'_inf_principal_eq, lift'_le, lift'_lift'_assoc, lift'_lift_assoc, lift'_map_le, lift'_mono, lift'_mono', lift'_neBot_iff, lift'_principal, lift'_pure, lift'_top, lift_assoc, lift_comm, lift_const, lift_iInf, lift_iInf_le, lift_iInf_of_directed, lift_iInf_of_map_univ, lift_inf, lift_le, lift_lift'_assoc, lift_lift'_same_eq_lift', lift_lift'_same_le_lift', lift_lift_same_eq_lift, lift_lift_same_le_lift, lift_map_le, lift_mono, lift_mono', lift_neBot_iff, lift_principal, lift_principal2, lift_top, map_lift'_eq, map_lift'_eq2, map_lift_eq, map_lift_eq2, mem_lift, mem_lift', mem_lift'_sets, mem_lift_sets, mem_prod_same_iff, monotone_lift, monotone_lift', principal_le_lift', prod_def, prod_lift'_lift', prod_lift_lift, prod_same_eq, sInter_lift'_sets, sInter_lift_sets, tendsto_lift, tendsto_lift', tendsto_prod_self_iff	70
Total	70

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_eq_lift' 📖	mathematical	—	comap lift' Set.preimage	—	ext mem_lift'_sets Set.monotone_preimage
comap_lift'_eq 📖	mathematical	—	comap lift' Set Set.preimage	—	comap_lift_eq comap_principal
comap_lift'_eq2 📖	mathematical	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	lift' comap Set.preimage	—	comap_lift_eq2 Monotone.comp monotone_principal
comap_lift_eq 📖	mathematical	—	comap lift Set Filter	—	comap_iInf
comap_lift_eq2 📖	mathematical	Monotone Set Filter PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder	lift comap Set.preimage	—	le_antisymm le_iInf₂ iInf₂_le Set.Subset.rfl iInf₂_le_of_le
eventually_lift'_iff 📖	mathematical	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	Eventually lift' Filter instMembership	—	mem_lift'_sets
le_lift 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder lift	—	le_iInf₂_iff
le_lift' 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder lift' Set instMembership	—	le_lift le_principal_iff
lift'_bot 📖	mathematical	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	lift' Bot.bot Filter instBot principal Set.instEmptyCollection	—	principal_empty lift'_principal
lift'_cong 📖	mathematical	—	lift'	—	le_antisymm lift'_mono' le_of_eq
lift'_iInf 📖	mathematical	Set Set.instInter	lift' iInf Filter instInfSet	—	lift_iInf inf_principal
lift'_iInf_of_map_univ 📖	mathematical	Set Set.instInter Set.univ	lift' iInf Filter instInfSet	—	lift_iInf_of_map_univ inf_principal principal_univ
lift'_id 📖	mathematical	—	lift' Set	—	lift_principal2
lift'_inf 📖	mathematical	Set Set.instInter	lift' Filter instInf	—	inf_eq_iInf lift'_iInf iInf_congr
lift'_inf_le 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder lift' instInf	—	le_inf lift'_mono inf_le_left le_rfl inf_le_right
lift'_inf_principal_eq 📖	mathematical	—	Filter instInf lift' principal Set Set.instInter	—	iInf_congr_Prop iInf_subtype'
lift'_le 📖	mathematical	Set Filter instMembership Preorder.toLE PartialOrder.toPreorder instPartialOrder principal	lift'	—	lift_le
lift'_lift'_assoc 📖	mathematical	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	lift'	—	lift_lift'_assoc Monotone.comp monotone_principal
lift'_lift_assoc 📖	mathematical	Monotone Set Filter PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder	lift' lift	—	lift_assoc
lift'_map_le 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder lift' map Set Set.image	—	lift_map_le
lift'_mono 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder Pi.hasLe Set Set.instLE	lift'	—	lift_mono principal_mono
lift'_mono' 📖	mathematical	Set Set.instHasSubset	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder lift'	—	iInf₂_mono principal_mono
lift'_neBot_iff 📖	mathematical	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	NeBot lift' Set.Nonempty	—	lift_neBot_iff Monotone.comp monotone_principal
lift'_principal 📖	mathematical	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	lift' principal	—	lift_principal Monotone.comp monotone_principal
lift'_pure 📖	mathematical	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	lift' Filter instPure principal Set.instSingletonSet	—	principal_singleton lift'_principal
lift'_top 📖	mathematical	—	lift' Top.top Filter instTop principal Set.univ	—	lift_top
lift_assoc 📖	mathematical	Monotone Set Filter PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder	lift	—	le_antisymm le_iInf₂ iInf_le_of_le iInf_le mem_lift_sets
lift_comm 📖	mathematical	—	lift	—	le_antisymm le_iInf iInf_le_of_le iInf_le
lift_const 📖	mathematical	—	lift	—	iInf_subtype' iInf_const
lift_iInf 📖	mathematical	Set Set.instInter Filter instInf	lift iInf instInfSet	—	LE.le.antisymm lift_iInf_le iInf_sets_induct iInf₂_le_of_le iInf_le univ_mem le_inf mem_lift_sets Monotone.of_map_inf
lift_iInf_le 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder lift iInf instInfSet	—	le_iInf lift_mono iInf_le le_rfl
lift_iInf_of_directed 📖	mathematical	Directed Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder Monotone Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	lift iInf instInfSet	—	LE.le.antisymm lift_iInf_le mem_lift_sets mem_iInf_of_directed mem_iInf_of_mem mem_lift
lift_iInf_of_map_univ 📖	mathematical	Set Set.instInter Filter instInf Set.univ Top.top instTop	lift iInf instInfSet	—	isEmpty_or_nonempty iInf_of_empty lift_top lift_iInf
lift_inf 📖	mathematical	—	lift Filter instInf	—	iInf_congr_Prop iInf_inf_eq
lift_le 📖	mathematical	Set Filter instMembership Preorder.toLE PartialOrder.toPreorder instPartialOrder	lift	—	iInf₂_le_of_le
lift_lift'_assoc 📖	mathematical	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Filter instPartialOrder	lift lift'	—	lift_assoc Monotone.comp monotone_principal lift_principal
lift_lift'_same_eq_lift' 📖	mathematical	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	lift lift'	—	lift_lift_same_eq_lift Monotone.comp monotone_principal
lift_lift'_same_le_lift' 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder lift lift'	—	lift_lift_same_le_lift
lift_lift_same_eq_lift 📖	mathematical	Monotone Set Filter PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder	lift	—	LE.le.antisymm lift_lift_same_le_lift le_lift lift_le inter_mem Set.inter_subset_left Set.inter_subset_right
lift_lift_same_le_lift 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder lift	—	le_lift lift_le le_rfl
lift_map_le 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder lift map Set Set.image	—	le_lift lift_le image_mem_map le_rfl
lift_mono 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder Pi.hasLe Set	lift	—	iInf_mono iInf_mono'
lift_mono' 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder	lift	—	iInf₂_mono
lift_neBot_iff 📖	mathematical	Monotone Set Filter PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder	NeBot lift	—	mem_lift_sets
lift_principal 📖	mathematical	Monotone Set Filter PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder	lift principal	—	LE.le.antisymm lift_le mem_principal_self le_rfl le_lift
lift_principal2 📖	mathematical	—	lift principal	—	le_antisymm mem_lift mem_principal_self le_iInf
lift_top 📖	mathematical	—	lift Top.top Filter instTop Set.univ	—	iInf_congr_Prop iInf_iInf_eq_left
map_lift'_eq 📖	mathematical	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	map lift' Set.image	—	map_lift_eq Monotone.comp monotone_principal map_principal
map_lift'_eq2 📖	mathematical	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	lift' map Set.image	—	map_lift_eq2 Monotone.comp monotone_principal
map_lift_eq 📖	mathematical	Monotone Set Filter PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder	map lift	—	Monotone.comp map_mono ext mem_lift_sets
map_lift_eq2 📖	mathematical	Monotone Set Filter PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder	lift map Set.image	—	LE.le.antisymm lift_map_le le_lift lift_le Set.image_preimage_subset
mem_lift 📖	mathematical	Set Filter instMembership	lift	—	le_principal_iff iInf_le_of_le
mem_lift' 📖	mathematical	Set Filter instMembership	lift'	—	le_principal_iff iInf_le_of_le le_rfl
mem_lift'_sets 📖	mathematical	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	Filter instMembership lift' Set.instHasSubset	—	mem_lift_sets Monotone.comp monotone_principal
mem_lift_sets 📖	mathematical	Monotone Set Filter PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder	instMembership lift	—	HasBasis.mem_lift_iff basis_sets
mem_prod_same_iff 📖	mathematical	—	Set Filter instMembership SProd.sprod instSProd Set.instHasSubset Set.instSProd	—	mem_prod_self_iff
monotone_lift 📖	mathematical	Monotone Filter PartialOrder.toPreorder instPartialOrder Pi.preorder Set	lift	—	lift_mono
monotone_lift' 📖	mathematical	Monotone Filter PartialOrder.toPreorder instPartialOrder Pi.preorder Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	lift'	—	lift'_mono
principal_le_lift' 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder principal lift' Set Set.instHasSubset	—	le_lift'
prod_def 📖	mathematical	—	SProd.sprod Filter instSProd lift lift' Set Set.instSProd	—	HasBasis.eq_biInf HasBasis.prod basis_sets iInf_and iInf_prod iInf_congr_Prop iInf_congr iInf_comm
prod_lift'_lift' 📖	mathematical	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	SProd.sprod Filter instSProd lift' lift Set.instSProd	—	prod_lift_lift Monotone.comp monotone_principal prod_principal_principal
prod_lift_lift 📖	mathematical	Monotone Set Filter PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder	SProd.sprod instSProd lift	—	prod_def lift_assoc lift_comm lift'_lift_assoc
prod_same_eq 📖	mathematical	—	SProd.sprod Filter instSProd lift' Set Set.instSProd	—	HasBasis.eq_biInf HasBasis.prod_self basis_sets
sInter_lift'_sets 📖	mathematical	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	Set.sInter setOf Filter instMembership lift' Set.iInter	—	sInter_lift_sets Monotone.comp monotone_principal Set.iInter₂_congr csInf_Ici
sInter_lift_sets 📖	mathematical	Monotone Set Filter PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder	Set.sInter setOf instMembership lift Set.iInter	—	mem_lift_sets Set.sInter_eq_biInter Set.iInter_exists Set.iInter_and Set.iInter_comm Set.iInter_congr_Prop
tendsto_lift 📖	mathematical	—	Tendsto lift	—	—
tendsto_lift' 📖	mathematical	—	Tendsto lift' Eventually Set Set.instMembership	—	—
tendsto_prod_self_iff 📖	mathematical	—	Tendsto SProd.sprod Filter instSProd Set instMembership Set.instMembership	—	—

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift' 📖	mathematical	Filter.HasBasis Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	Filter.lift'	—	mem_lift_iff Filter.hasBasis_principal Monotone.comp Filter.monotone_principal
mem_lift_iff 📖	mathematical	Filter.HasBasis Monotone Set Filter PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Filter.instPartialOrder	Filter.instMembership Filter.lift Set.instHasSubset	—	Filter.mem_biInf_of_directed Filter.inter_mem Set.inter_subset_left Set.inter_subset_right Filter.univ_sets mem_iff exists_iff

---

← Back to Index