Loogle!

Result

Found 21 declarations mentioning Sublattice.map.

• Sublattice.map 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : Sublattice α) : Sublattice β
• Sublattice.map_id 📋 Mathlib.Order.Sublattice
  {α : Type u_2} [Lattice α] {L : Sublattice α} : Sublattice.map (LatticeHom.id α) L = L
• Sublattice.map_bot 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) : Sublattice.map f ⊥ = ⊥
• Sublattice.map_top 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (h : Function.Surjective ⇑f) : Sublattice.map f ⊤ = ⊤
• Sublattice.map_map 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [Lattice β] [Lattice γ] {L : Sublattice α} (g : LatticeHom β γ) (f : LatticeHom α β) : Sublattice.map g (Sublattice.map f L) = Sublattice.map (g.comp f) L
• Sublattice.map_mono 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {f : LatticeHom α β} : Monotone (Sublattice.map f)
• Sublattice.coe_map 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : Sublattice α) : ↑(Sublattice.map f L) = ⇑f '' ↑L
• Sublattice.gc_map_comap 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) : GaloisConnection (Sublattice.map f) (Sublattice.comap f)
• Sublattice.mem_map_of_mem 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} (f : LatticeHom α β) {a : α} : a ∈ L → f a ∈ Sublattice.map f L
• Sublattice.map_iSup 📋 Mathlib.Order.Sublattice
  {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : ι → Sublattice α) : Sublattice.map f (⨆ i, L i) = ⨆ i, Sublattice.map f (L i)
• Sublattice.map_inf 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L M : Sublattice α) (f : LatticeHom α β) (hf : Function.Injective ⇑f) : Sublattice.map f (L ⊓ M) = Sublattice.map f L ⊓ Sublattice.map f M
• Sublattice.mem_map 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {f : LatticeHom α β} {b : β} : b ∈ Sublattice.map f L ↔ ∃ a ∈ L, f a = b
• Sublattice.map_inf_le 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L M : Sublattice α) (f : LatticeHom α β) : Sublattice.map f (L ⊓ M) ≤ Sublattice.map f L ⊓ Sublattice.map f M
• Sublattice.map_le_iff_le_comap 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {f : LatticeHom α β} {M : Sublattice β} : Sublattice.map f L ≤ M ↔ L ≤ Sublattice.comap f M
• Sublattice.apply_mem_map_iff 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {f : LatticeHom α β} {a : α} (hf : Function.Injective ⇑f) : f a ∈ Sublattice.map f L ↔ a ∈ L
• Sublattice.apply_coe_mem_map 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} (f : LatticeHom α β) (a : ↥L) : f ↑a ∈ Sublattice.map f L
• Sublattice.map_sup 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L M : Sublattice α) : Sublattice.map f (L ⊔ M) = Sublattice.map f L ⊔ Sublattice.map f M
• Sublattice.mem_map_equiv 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {f : α ≃o β} {a : β} : a ∈ Sublattice.map { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ } L ↔ f.symm a ∈ L
• Sublattice.comap_equiv_eq_map_symm 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : β ≃o α) (L : Sublattice α) : Sublattice.comap { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ } L = Sublattice.map { toFun := ⇑f.symm, map_sup' := ⋯, map_inf' := ⋯ } L
• Sublattice.map_equiv_eq_comap_symm 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : α ≃o β) (L : Sublattice α) : Sublattice.map { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ } L = Sublattice.comap { toFun := ⇑f.symm, map_sup' := ⋯, map_inf' := ⋯ } L
• Sublattice.map_symm_eq_iff_eq_map 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {M : Sublattice β} {e : β ≃o α} : Sublattice.map { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ } L = M ↔ L = Sublattice.map { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ } M

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