Loogle!

Result

Found 31 declarations mentioning OmegaCompletePartialOrder.Chain.map.

• OmegaCompletePartialOrder.Chain.map 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) (f : α →o β) : OmegaCompletePartialOrder.Chain β
• OmegaCompletePartialOrder.Chain.map_id 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} [Preorder α] (c : OmegaCompletePartialOrder.Chain α) : c.map OrderHom.id = c
• OmegaCompletePartialOrder.Chain.map_comp 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} (g : β →o γ) : (c.map f).map g = c.map (g.comp f)
• OmegaCompletePartialOrder.Chain.mem_map 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} (x : α) : x ∈ c → f x ∈ c.map f
• OmegaCompletePartialOrder.Chain.map_le_map 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) {f g : α →o β} (h : f ≤ g) : c.map f ≤ c.map g
• OmegaCompletePartialOrder.Chain.exists_of_mem_map 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} {b : β} : b ∈ c.map f → ∃ a ∈ c, f a = b
• OmegaCompletePartialOrder.Chain.map_coe 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) (f : α →o β) : ⇑(c.map f) = ⇑f ∘ ⇑c
• OmegaCompletePartialOrder.Chain.mem_map_iff 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} {b : β} : b ∈ c.map f ↔ ∃ a ∈ c, f a = b
• OmegaCompletePartialOrder.ContinuousHom.map_ωSup' 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (self : α →𝒄 β) (c : OmegaCompletePartialOrder.Chain α) : self.toFun (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map self.toOrderHom)
• OmegaCompletePartialOrder.ωScottContinuous.map_ωSup 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α → β} (hf : OmegaCompletePartialOrder.ωScottContinuous f) (c : OmegaCompletePartialOrder.Chain α) : f (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map { toFun := f, monotone' := ⋯ })
• OmegaCompletePartialOrder.ContinuousHom.mk 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (toOrderHom : α →o β) (map_ωSup' : ∀ (c : OmegaCompletePartialOrder.Chain α), toOrderHom.toFun (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map toOrderHom)) : α →𝒄 β
• Prod.ωSup_fst 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α × β)) : (Prod.ωSup c).1 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.fst)
• Prod.ωSup_snd 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α × β)) : (Prod.ωSup c).2 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.snd)
• Prod.instOmegaCompletePartialOrder_ωSup_fst 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α × β)) : (OmegaCompletePartialOrder.ωSup c).1 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.fst)
• Prod.instOmegaCompletePartialOrder_ωSup_snd 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α × β)) : (OmegaCompletePartialOrder.ωSup c).2 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.snd)
• OmegaCompletePartialOrder.ContinuousHom.continuous 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (F : α →𝒄 β) (C : OmegaCompletePartialOrder.Chain α) : F (OmegaCompletePartialOrder.ωSup C) = OmegaCompletePartialOrder.ωSup (C.map ↑F)
• OmegaCompletePartialOrder.ωScottContinuous.monotone_map_ωSup 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α → β} : OmegaCompletePartialOrder.ωScottContinuous f → ∃ (hf : Monotone f), ∀ (c : OmegaCompletePartialOrder.Chain α), f (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map { toFun := f, monotone' := hf })
• OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α → β} : (∃ (hf : Monotone f), ∀ (c : OmegaCompletePartialOrder.Chain α), f (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map { toFun := f, monotone' := hf })) → OmegaCompletePartialOrder.ωScottContinuous f
• OmegaCompletePartialOrder.ωScottContinuous_iff_monotone_map_ωSup 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α → β} : OmegaCompletePartialOrder.ωScottContinuous f ↔ ∃ (hf : Monotone f), ∀ (c : OmegaCompletePartialOrder.Chain α), f (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map { toFun := f, monotone' := hf })
• OmegaCompletePartialOrder.ωScottContinuous.isLUB 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α → β} {c : OmegaCompletePartialOrder.Chain α} (hf : OmegaCompletePartialOrder.ωScottContinuous f) : IsLUB (Set.range ⇑(c.map { toFun := f, monotone' := ⋯ })) (f (OmegaCompletePartialOrder.ωSup c))
• OmegaCompletePartialOrder.ωScottContinuous.map_ωSup_of_orderHom 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α →o β} : OmegaCompletePartialOrder.ωScottContinuous ⇑f → ∀ (c : OmegaCompletePartialOrder.Chain α), f (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map f)
• OmegaCompletePartialOrder.ωScottContinuous.of_map_ωSup_of_orderHom 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α →o β} : (∀ (c : OmegaCompletePartialOrder.Chain α), f (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map f)) → OmegaCompletePartialOrder.ωScottContinuous ⇑f
• OmegaCompletePartialOrder.ωScottContinuous_iff_map_ωSup_of_orderHom 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α →o β} : OmegaCompletePartialOrder.ωScottContinuous ⇑f ↔ ∀ (c : OmegaCompletePartialOrder.Chain α), f (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map f)
• OmegaCompletePartialOrder.ContinuousHom.coe_mk 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →o β) (hf : ∀ (c : OmegaCompletePartialOrder.Chain α), f.toFun (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map f)) : ⇑{ toOrderHom := f, map_ωSup' := hf } = ⇑f
• OmegaCompletePartialOrder.OrderHom.ωSup_coe 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α →o β)) (a : α) : (OmegaCompletePartialOrder.OrderHom.ωSup c) a = OmegaCompletePartialOrder.ωSup (c.map (OrderHom.apply a))
• OmegaCompletePartialOrder.ContinuousHom.mk.sizeOf_spec 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] [SizeOf α] [SizeOf β] (toOrderHom : α →o β) (map_ωSup' : ∀ (c : OmegaCompletePartialOrder.Chain α), toOrderHom.toFun (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map toOrderHom)) : sizeOf { toOrderHom := toOrderHom, map_ωSup' := map_ωSup' } = 1 + sizeOf toOrderHom
• OmegaCompletePartialOrder.OrderHom.omegaCompletePartialOrder_ωSup_coe 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α →o β)) (a : α) : (OmegaCompletePartialOrder.ωSup c) a = OmegaCompletePartialOrder.ωSup (c.map (OrderHom.apply a))
• OmegaCompletePartialOrder.lift 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [PartialOrder β] (f : β →o α) (ωSup₀ : OmegaCompletePartialOrder.Chain β → β) (h : ∀ (x y : β), f x ≤ f y → x ≤ y) (h' : ∀ (c : OmegaCompletePartialOrder.Chain β), f (ωSup₀ c) = OmegaCompletePartialOrder.ωSup (c.map f)) : OmegaCompletePartialOrder β
• OmegaCompletePartialOrder.ContinuousHom.ωSup_bind 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} [OmegaCompletePartialOrder α] {β γ : Type v} (c : OmegaCompletePartialOrder.Chain α) (f : α →o Part β) (g : α →o β → Part γ) : OmegaCompletePartialOrder.ωSup (c.map (f.partBind g)) = OmegaCompletePartialOrder.ωSup (c.map f) >>= OmegaCompletePartialOrder.ωSup (c.map g)
• OmegaCompletePartialOrder.ContinuousHom.mk.injEq 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (toOrderHom : α →o β) (map_ωSup' : ∀ (c : OmegaCompletePartialOrder.Chain α), toOrderHom.toFun (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map toOrderHom)) (toOrderHom✝ : α →o β) (map_ωSup'✝ : ∀ (c : OmegaCompletePartialOrder.Chain α), toOrderHom✝.toFun (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map toOrderHom✝)) : ({ toOrderHom := toOrderHom, map_ωSup' := map_ωSup' } = { toOrderHom := toOrderHom✝, map_ωSup' := map_ωSup'✝ }) = (toOrderHom = toOrderHom✝)
• OmegaCompletePartialOrder.ContinuousHom.ωSup_apply 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α →𝒄 β)) (a : α) : (OmegaCompletePartialOrder.ContinuousHom.ωSup c) a = OmegaCompletePartialOrder.ωSup ((c.map OmegaCompletePartialOrder.ContinuousHom.toMono).map (OrderHom.apply a))

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision bce1d65