Loogle!

Result

Found 21 declarations mentioning BooleanSubalgebra.map.

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