Mathlib Map

Theorems · Theorem · order theory

OrderIso.map_bot

∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : PartialOrder β] [inst_2 : OrderBot α] [inst_3 : OrderBot β]
  (f : α ≃o β), f ⊥ = ⊥
Defined in
Mathlib.Order.Hom.Basic
Cited by
30 results in Mathlib
Foundations
Depth 27 from the axioms · uses propext, Quot.sound
Assumes
LEPartialOrderOrderBotOrderBot
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

OrderIso.isAtom_iff · cited by 5OrderIso.isAtom_iffMulAction.isCoatom_stabilizer_iff_preprimitive · cited by 4MulAction.isCoatom_stabil…Cardinal.preAleph_zero · cited by 3Cardinal.preAleph_zeroDisjoint.map_orderIso · cited by 3Disjoint.map_orderIsomap_prime_of_factor_orderIso · cited by 2map_prime_of_factor_order…IsGalois.tfae · cited by 2IsGalois.tfaeAddSubgroup.unop_bot · cited by 1AddSubgroup.unop_botSubsemiring.unop_bot · cited by 1Subsemiring.unop_botSubsemigroup.op_bot · cited by 1Subsemigroup.op_botAddSubmonoid.op_bot · cited by 1AddSubmonoid.op_botSubsemigroup.unop_bot · cited by 1Subsemigroup.unop_botProjectivization.Subspace.bot_coe · cited by 1Subspace.bot_coeOrderIso.map_ciSup' · cited by 1OrderIso.map_ciSup'Subring.unop_bot · cited by 1Subring.unop_botAddAction.isCoatom_stabilizer_iff_preprimitive · cited by 1AddAction.isCoatom_stabil…DFunLike.coe · cited by 62936DFunLike.coePartialOrder · cited by 6410PartialOrderBot.bot · cited by 4720Bot.botOrderBot · cited by 1055OrderBotOrderIso · cited by 874OrderIsobot_le · cited by 306bot_leOrderIso.map_bot' · cited by 1OrderIso.map_bot'OrderIso.map_botCITED BYCITES

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by30

Results whose statement or proof uses this declaration.