Loogle!

Result

Found 156 declarations mentioning HImp.himp.

• HImp.himp 📋 Mathlib.Order.Notation
  {α : Type u_1} [self : HImp α] : α → α → α
• Pi.himp_apply 📋 Mathlib.Order.Basic
  {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → HImp (π i)] (x y : (i : ι) → π i) (i : ι) : (y ⇨ x) i = y i ⇨ x i
• Pi.himp_def 📋 Mathlib.Order.Basic
  {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → HImp (π i)] (x y : (i : ι) → π i) : y ⇨ x = fun i => y i ⇨ x i
• Equiv.himp_def 📋 Mathlib.Order.OrderDual
  {α : Type u_1} {β : Type u_2} (e : α ≃ β) [HImp β] (a b : α) : a ⇨ b = e.symm (e a ⇨ e b)
• himp_iff_imp 📋 Mathlib.Order.Heyting.Basic
  (p q : Prop) : p ⇨ q ↔ p → q
• PUnit.himp_eq 📋 Mathlib.Order.Heyting.Basic
  (a b : PUnit.{u + 1}) : a ⇨ b = PUnit.unit
• himp_compl 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] (a : α) : a ⇨ aᶜ = aᶜ
• himp_eq_himp_iff 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} : b ⇨ a = a ⇨ b ↔ a = b
• himp_ne_himp_iff 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} : b ⇨ a ≠ a ⇨ b ↔ a ≠ b
• le_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} : a ≤ b ⇨ a
• himp_idem 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} : b ⇨ b ⇨ a = b ⇨ a
• Codisjoint.himp_eq_left 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} (h : Codisjoint a b) : a ⇨ b = b
• Codisjoint.himp_eq_right 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} (h : Codisjoint a b) : b ⇨ a = a
• himp_self 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} : a ⇨ a = ⊤
• sup_himp_self_left 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) : a ⊔ b ⇨ a = b ⇨ a
• sup_himp_self_right 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) : a ⊔ b ⇨ b = a ⇨ b
• top_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} : ⊤ ⇨ a = a
• le_himp_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} : a ≤ (a ⇨ b) ⇨ b
• himp_left_comm 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b c : α) : a ⇨ b ⇨ c = b ⇨ a ⇨ c
• compl_le_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] {a b : α} : aᶜ ≤ a ⇨ b
• himp_compl_comm 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] (a b : α) : a ⇨ bᶜ = b ⇨ aᶜ
• himp_inf_self 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) : (a ⇨ b) ⊓ a = b ⊓ a
• inf_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) : a ⊓ (a ⇨ b) = a ⊓ b
• himp_inf_le 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} : (a ⇨ b) ⊓ a ≤ b
• inf_himp_le 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} : a ⊓ (a ⇨ b) ≤ b
• himp_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b c : α) : a ⇨ b ⇨ c = a ⊓ b ⇨ c
• fst_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} {β : Type u_3} [HImp α] [HImp β] (a b : α × β) : (a ⇨ b).1 = a.1 ⇨ b.1
• snd_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} {β : Type u_3} [HImp α] [HImp β] (a b : α × β) : (a ⇨ b).2 = a.2 ⇨ b.2
• Codisjoint.himp_inf_cancel_left 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} (h : Codisjoint a b) : a ⇨ a ⊓ b = b
• Codisjoint.himp_inf_cancel_right 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} (h : Codisjoint a b) : b ⇨ a ⊓ b = a
• himp_bot 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] (a : α) : a ⇨ ⊥ = aᶜ
• HeytingAlgebra.himp_bot 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_4} [self : HeytingAlgebra α] (a : α) : a ⇨ ⊥ = aᶜ
• le_himp_iff_left 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} : a ≤ a ⇨ b ↔ a ≤ b
• gc_inf_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} : GaloisConnection (fun x => a ⊓ x) fun x => a ⇨ x
• himp_le_himp_himp_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b c : α} : b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c
• compl_sup_le_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] {a b : α} : aᶜ ⊔ b ≤ a ⇨ b
• sup_compl_le_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] {a b : α} : b ⊔ aᶜ ≤ a ⇨ b
• himp_eq_top_iff 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} : a ⇨ b = ⊤ ↔ a ≤ b
• himp_inf_distrib 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b c : α) : a ⇨ b ⊓ c = (a ⇨ b) ⊓ (a ⇨ c)
• himp_le_himp_left 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b c : α} (h : a ≤ b) : c ⇨ a ≤ c ⇨ b
• himp_le_himp_right 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b c : α} (h : a ≤ b) : b ⇨ c ≤ a ⇨ c
• himp_top 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} : a ⇨ ⊤ = ⊤
• sup_himp_distrib 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b c : α) : a ⊔ b ⇨ c = (a ⇨ c) ⊓ (b ⇨ c)
• himp_triangle 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b c : α) : (a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c
• le_himp_comm 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b c : α} : a ≤ b ⇨ c ↔ b ≤ a ⇨ c
• HeytingAlgebra.mk 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_4} [toGeneralizedHeytingAlgebra : GeneralizedHeytingAlgebra α] [toOrderBot : OrderBot α] [toCompl : Compl α] (himp_bot : ∀ (a : α), a ⇨ ⊥ = aᶜ) : HeytingAlgebra α
• himp_inf_himp_inf_le 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b c : α} : (b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c
• le_himp_iff 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b c : α} : a ≤ b ⇨ c ↔ a ⊓ b ≤ c
• le_himp_iff' 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b c : α} : a ≤ b ⇨ c ↔ b ⊓ a ≤ c
• compl_compl_himp_distrib 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] (a b : α) : (a ⇨ b)ᶜᶜ = aᶜᶜ ⇨ bᶜᶜ
• Codisjoint.himp_le_of_right_le 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b c : α} (hac : Codisjoint a c) (hba : b ≤ a) : c ⇨ b ≤ a
• himp_le_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) : b ⇨ c ≤ a ⇨ d
• himp_inf_himp_cancel 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b c : α} (hba : b ≤ a) (hcb : c ≤ b) : (a ⇨ b) ⊓ (b ⇨ c) = a ⇨ c
• bot_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] (a : α) : ⊥ ⇨ a = ⊤
• GeneralizedHeytingAlgebra.mk 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_4} [toLattice : Lattice α] [toOrderTop : OrderTop α] [toHImp : HImp α] (le_himp_iff : ∀ (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c) : GeneralizedHeytingAlgebra α
• GeneralizedHeytingAlgebra.le_himp_iff 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_4} [self : GeneralizedHeytingAlgebra α] (a b c : α) : a ≤ b ⇨ c ↔ a ⊓ b ≤ c
• toDual_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] (a b : α) : OrderDual.toDual (a ⇨ b) = OrderDual.toDual b \ OrderDual.toDual a
• toDual_sdiff 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [CoheytingAlgebra α] (a b : α) : OrderDual.toDual (b \ a) = OrderDual.toDual a ⇨ OrderDual.toDual b
• ofDual_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [CoheytingAlgebra α] (a b : αᵒᵈ) : OrderDual.ofDual (b ⇨ a) = OrderDual.ofDual a \ OrderDual.ofDual b
• ofDual_sdiff 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] (a b : αᵒᵈ) : OrderDual.ofDual (a \ b) = OrderDual.ofDual b ⇨ OrderDual.ofDual a
• Function.Injective.generalizedHeytingAlgebra 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} {β : Type u_3} [Max α] [Min α] [LE α] [LT α] [Top α] [HImp α] [GeneralizedHeytingAlgebra β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_top : f ⊤ = ⊤) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) : GeneralizedHeytingAlgebra α
• Function.Injective.heytingAlgebra 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} {β : Type u_3} [Max α] [Min α] [LE α] [LT α] [Top α] [Bot α] [Compl α] [HImp α] [HeytingAlgebra β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) : HeytingAlgebra α
• Function.Injective.biheytingAlgebra 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} {β : Type u_3} [Max α] [Min α] [LE α] [LT α] [Top α] [Bot α] [Compl α] [HNot α] [HImp α] [SDiff α] [BiheytingAlgebra β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ) (map_hnot : ∀ (a : α), f (￢a) = ￢f a) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) : BiheytingAlgebra α
• BooleanAlgebra.himp_eq 📋 Mathlib.Order.BooleanAlgebra.Defs
  {α : Type u} [self : BooleanAlgebra α] (x y : α) : x ⇨ y = y ⊔ xᶜ
• BooleanAlgebra.mk 📋 Mathlib.Order.BooleanAlgebra.Defs
  {α : Type u} [toDistribLattice : DistribLattice α] [toCompl : Compl α] [toSDiff : SDiff α] [toHImp : HImp α] [toTop : Top α] [toBot : Bot α] (inf_compl_le_bot : ∀ (x : α), x ⊓ xᶜ ≤ ⊥) (top_le_sup_compl : ∀ (x : α), ⊤ ≤ x ⊔ xᶜ) (le_top : ∀ (a : α), a ≤ ⊤) (bot_le : ∀ (a : α), ⊥ ≤ a) (sdiff_eq : ∀ (x y : α), x \ y = x ⊓ yᶜ := by aesop) (himp_eq : ∀ (x y : α), x ⇨ y = y ⊔ xᶜ := by aesop) : BooleanAlgebra α
• compl_himp 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [BooleanAlgebra α] : (x ⇨ y)ᶜ = x \ y
• compl_sdiff 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [BooleanAlgebra α] : (x \ y)ᶜ = x ⇨ y
• compl_himp_compl 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [BooleanAlgebra α] : xᶜ ⇨ yᶜ = y ⇨ x
• himp_eq 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [BooleanAlgebra α] : x ⇨ y = y ⊔ xᶜ
• himp_eq_left 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [BooleanAlgebra α] : x ⇨ y = x ↔ x = ⊤ ∧ y = ⊤
• himp_ne_right 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [BooleanAlgebra α] : x ⇨ y ≠ x ↔ x ≠ ⊤ ∨ y ≠ ⊤
• codisjoint_himp_self_left 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [BooleanAlgebra α] : Codisjoint (x ⇨ y) x
• codisjoint_himp_self_right 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [BooleanAlgebra α] : Codisjoint x (x ⇨ y)
• himp_le_left 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [BooleanAlgebra α] : x ⇨ y ≤ x ↔ x = ⊤
• himp_le 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y z : α} [BooleanAlgebra α] : x ⇨ y ≤ z ↔ y ≤ z ∧ Codisjoint x z
• Function.Injective.booleanAlgebra 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {β : Type u_1} [Max α] [Min α] [LE α] [LT α] [Top α] [Bot α] [Compl α] [SDiff α] [HImp α] [BooleanAlgebra β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) : BooleanAlgebra α
• Set.himp_def 📋 Mathlib.Order.BooleanAlgebra.Set
  {α : Type u_1} {s t : Set α} : s ⇨ t = t ∪ sᶜ
• Set.mem_himp_iff 📋 Mathlib.Order.BooleanAlgebra.Set
  {α : Type u_1} {s t : Set α} {a : α} : a ∈ s ⇨ t ↔ a ∈ s → a ∈ t
• bihimp_def 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [Min α] [HImp α] (a b : α) : bihimp a b = (b ⇨ a) ⊓ (a ⇨ b)
• bihimp_himp_eq_inf 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) : bihimp a (a ⇨ b) = a ⊓ b
• himp_bihimp_eq_inf 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) : bihimp (b ⇨ a) b = a ⊓ b
• himp_bihimp_left 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [BooleanAlgebra α] (a b : α) : a ⇨ bihimp a b = a ⇨ b
• himp_bihimp_right 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [BooleanAlgebra α] (a b : α) : b ⇨ bihimp a b = b ⇨ a
• bihimp_of_ge 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} (h : a ≤ b) : bihimp a b = b ⇨ a
• bihimp_of_le 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} (h : b ≤ a) : bihimp a b = a ⇨ b
• bihimp_eq_sup_himp_inf 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) : bihimp a b = a ⊔ b ⇨ a ⊓ b
• bihimp_himp_left 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [BooleanAlgebra α] (a b : α) : bihimp a b ⇨ a = a ⊔ b
• bihimp_himp_right 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [BooleanAlgebra α] (a b : α) : bihimp a b ⇨ b = a ⊔ b
• sup_himp_bihimp 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) : a ⊔ b ⇨ bihimp a b = bihimp a b
• inf_himp_bihimp 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [BooleanAlgebra α] (a b : α) : bihimp a b ⇨ a ⊓ b = a ⊔ b
• himp_bihimp 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b c : α) : c ⇨ bihimp a b = (b ⊓ c ⇨ a) ⊓ (a ⊓ c ⇨ b)
• isGreatest_himp 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [GeneralizedHeytingAlgebra α] (a b : α) : IsGreatest {w | w ⊓ a ≤ b} (a ⇨ b)
• CompleteLinearOrder.himp_bot 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_4} [self : CompleteLinearOrder α] (a : α) : a ⇨ ⊥ = aᶜ
• CompleteLinearOrder.le_himp_iff 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_4} [self : CompleteLinearOrder α] (a b c : α) : a ≤ b ⇨ c ↔ min a b ≤ c
• CompleteLinearOrder.mk 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_4} [toCompleteLattice : CompleteLattice α] [toHImp : HImp α] (le_himp_iff : ∀ (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c) [toCompl : Compl α] (himp_bot : ∀ (a : α), a ⇨ ⊥ = aᶜ) [toSDiff : SDiff α] (sdiff_le_iff : ∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c) [toHNot : HNot α] (top_sdiff : ∀ (a : α), ⊤ \ a = ￢a) [toOrd : Ord α] (le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a) (toDecidableLE : DecidableLE α) (toDecidableEq : DecidableEq α) (toDecidableLT : DecidableLT α) (compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b := by compareOfLessAndEq_rfl) : CompleteLinearOrder α
• CompleteBooleanAlgebra.himp_eq 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u_1} [self : CompleteBooleanAlgebra α] (x y : α) : x ⇨ y = y ⊔ xᶜ
• himp_iInf_eq 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} {ι : Sort w} [Order.Frame α] {a : α} {f : ι → α} : a ⇨ ⨅ x, f x = ⨅ x, a ⇨ f x
• iSup_himp_eq 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} {ι : Sort w} [Order.Frame α] {a : α} {f : ι → α} : (⨆ x, f x) ⇨ a = ⨅ x, f x ⇨ a
• CompletelyDistribLattice.himp_bot 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} [self : CompletelyDistribLattice α] (a : α) : a ⇨ ⊥ = aᶜ
• Order.Frame.himp_bot 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u_1} [self : Order.Frame α] (a : α) : a ⇨ ⊥ = aᶜ
• himp_eq_sSup 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} [Order.Frame α] {a b : α} : a ⇨ b = sSup {w | w ⊓ a ≤ b}
• himp_le_iff 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} [Order.Frame α] {a b c : α} : a ⇨ b ≤ c ↔ ∀ (d : α), d ⊓ a ≤ b → d ≤ c
• CompletelyDistribLattice.le_himp_iff 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} [self : CompletelyDistribLattice α] (a b c : α) : a ≤ b ⇨ c ↔ a ⊓ b ≤ c
• Order.Frame.le_himp_iff 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u_1} [self : Order.Frame α] (a b c : α) : a ≤ b ⇨ c ↔ a ⊓ b ≤ c
• Order.Frame.mk 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u_1} [toCompleteLattice : CompleteLattice α] [toHImp : HImp α] (le_himp_iff : ∀ (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c) [toCompl : Compl α] (himp_bot : ∀ (a : α), a ⇨ ⊥ = aᶜ) : Order.Frame α
• CompletelyDistribLattice.mk 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} [toCompleteLattice : CompleteLattice α] [toHImp : HImp α] (le_himp_iff : ∀ (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c) [toCompl : Compl α] (himp_bot : ∀ (a : α), a ⇨ ⊥ = aᶜ) [toSDiff : SDiff α] (sdiff_le_iff : ∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c) [toHNot : HNot α] (top_sdiff : ∀ (a : α), ⊤ \ a = ￢a) (iInf_iSup_eq : ∀ {ι : Type u} {κ : ι → Type u} (f : (a : ι) → κ a → α), ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)) : CompletelyDistribLattice α
• Function.Injective.completeBooleanAlgebra 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} {β : Type v} [Max α] [Min α] [LE α] [LT α] [SupSet α] [InfSet α] [Top α] [Bot α] [Compl α] [HImp α] [SDiff α] [CompleteBooleanAlgebra β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) : CompleteBooleanAlgebra α
• Function.Injective.frame 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} {β : Type v} [Max α] [Min α] [LE α] [LT α] [SupSet α] [InfSet α] [Top α] [Bot α] [Compl α] [HImp α] [Order.Frame β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) : Order.Frame α
• CompleteBooleanAlgebra.mk 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u_1} [toCompleteLattice : CompleteLattice α] (le_sup_inf : ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z) [toCompl : Compl α] [toSDiff : SDiff α] [toHImp : HImp α] (inf_compl_le_bot : ∀ (x : α), x ⊓ xᶜ ≤ ⊥) (top_le_sup_compl : ∀ (x : α), ⊤ ≤ x ⊔ xᶜ) (sdiff_eq : ∀ (x y : α), x \ y = x ⊓ yᶜ := by aesop) (himp_eq : ∀ (x y : α), x ⇨ y = y ⊔ xᶜ := by aesop) : CompleteBooleanAlgebra α
• Function.Injective.completeAtomicBooleanAlgebra 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} {β : Type v} [Max α] [Min α] [LE α] [LT α] [SupSet α] [InfSet α] [Top α] [Bot α] [Compl α] [HImp α] [HNot α] [SDiff α] [CompleteAtomicBooleanAlgebra β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) (map_hnot : ∀ (a : α), f (￢a) = ￢f a) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) : CompleteAtomicBooleanAlgebra α
• Function.Injective.completeDistribLattice 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} {β : Type v} [Max α] [Min α] [LE α] [LT α] [SupSet α] [InfSet α] [Top α] [Bot α] [Compl α] [HImp α] [HNot α] [SDiff α] [CompleteDistribLattice β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) (map_hnot : ∀ (a : α), f (￢a) = ￢f a) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) : CompleteDistribLattice α
• Function.Injective.completelyDistribLattice 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} {β : Type v} [Max α] [Min α] [LE α] [LT α] [SupSet α] [InfSet α] [Top α] [Bot α] [Compl α] [HImp α] [HNot α] [SDiff α] [CompletelyDistribLattice β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) (map_hnot : ∀ (a : α), f (￢a) = ￢f a) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) : CompletelyDistribLattice α
• Finset.himp_def 📋 Mathlib.Data.Finset.BooleanAlgebra
  {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] : s ⇨ t = t ∪ sᶜ
• Finset.mem_himp_iff 📋 Mathlib.Data.Finset.BooleanAlgebra
  {α : Type u_1} {s t : Finset α} [Fintype α] [DecidableEq α] {a : α} : a ∈ s ⇨ t ↔ a ∈ s → a ∈ t
• Finset.inf_himp_right 📋 Mathlib.Data.Finset.Lattice.Fold
  {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] (s : Finset ι) (f : ι → α) (a : α) : (s.inf fun b => f b ⇨ a) = s.sup f ⇨ a
• Finset.sup_himp_left 📋 Mathlib.Data.Finset.Lattice.Fold
  {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α) : (s.sup fun b => a ⇨ f b) = a ⇨ s.sup f
• Finset.sup_himp_right 📋 Mathlib.Data.Finset.Lattice.Fold
  {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α) : (s.sup fun b => f b ⇨ a) = s.inf f ⇨ a
• HeytingHomClass.map_himp 📋 Mathlib.Order.Heyting.Hom
  {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst✝ : HeytingAlgebra α} {inst✝¹ : HeytingAlgebra β} {inst✝² : FunLike F α β} [self : HeytingHomClass F α β] (f : F) (a b : α) : f (a ⇨ b) = f a ⇨ f b
• BiheytingHomClass.map_himp 📋 Mathlib.Order.Heyting.Hom
  {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst✝ : BiheytingAlgebra α} {inst✝¹ : BiheytingAlgebra β} {inst✝² : FunLike F α β} [self : BiheytingHomClass F α β] (f : F) (a b : α) : f (a ⇨ b) = f a ⇨ f b
• HeytingHomClass.mk 📋 Mathlib.Order.Heyting.Hom
  {F : Type u_6} {α : Type u_7} {β : Type u_8} [HeytingAlgebra α] [HeytingAlgebra β] [FunLike F α β] [toLatticeHomClass : LatticeHomClass F α β] (map_bot : ∀ (f : F), f ⊥ = ⊥) (map_himp : ∀ (f : F) (a b : α), f (a ⇨ b) = f a ⇨ f b) : HeytingHomClass F α β
• BiheytingHomClass.mk 📋 Mathlib.Order.Heyting.Hom
  {F : Type u_6} {α : Type u_7} {β : Type u_8} [BiheytingAlgebra α] [BiheytingAlgebra β] [FunLike F α β] [toLatticeHomClass : LatticeHomClass F α β] (map_himp : ∀ (f : F) (a b : α), f (a ⇨ b) = f a ⇨ f b) (map_sdiff : ∀ (f : F) (a b : α), f (a \ b) = f a \ f b) : BiheytingHomClass F α β
• HeytingHom.map_himp' 📋 Mathlib.Order.Heyting.Hom
  {α : Type u_6} {β : Type u_7} [HeytingAlgebra α] [HeytingAlgebra β] (self : HeytingHom α β) (a b : α) : self.toFun (a ⇨ b) = self.toFun a ⇨ self.toFun b
• BiheytingHom.map_himp' 📋 Mathlib.Order.Heyting.Hom
  {α : Type u_6} {β : Type u_7} [BiheytingAlgebra α] [BiheytingAlgebra β] (self : BiheytingHom α β) (a b : α) : self.toFun (a ⇨ b) = self.toFun a ⇨ self.toFun b
• HeytingHom.mk 📋 Mathlib.Order.Heyting.Hom
  {α : Type u_6} {β : Type u_7} [HeytingAlgebra α] [HeytingAlgebra β] (toLatticeHom : LatticeHom α β) (map_bot' : toLatticeHom.toFun ⊥ = ⊥) (map_himp' : ∀ (a b : α), toLatticeHom.toFun (a ⇨ b) = toLatticeHom.toFun a ⇨ toLatticeHom.toFun b) : HeytingHom α β
• BiheytingHom.mk 📋 Mathlib.Order.Heyting.Hom
  {α : Type u_6} {β : Type u_7} [BiheytingAlgebra α] [BiheytingAlgebra β] (toLatticeHom : LatticeHom α β) (map_himp' : ∀ (a b : α), toLatticeHom.toFun (a ⇨ b) = toLatticeHom.toFun a ⇨ toLatticeHom.toFun b) (map_sdiff' : ∀ (a b : α), toLatticeHom.toFun (a \ b) = toLatticeHom.toFun a \ toLatticeHom.toFun b) : BiheytingHom α β
• IsClopen.himp 📋 Mathlib.Topology.Clopen
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ⇨ t)
• BooleanSubalgebra.himp_mem 📋 Mathlib.Order.BooleanSubalgebra
  {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} {a b : α} (ha : a ∈ L) (hb : b ∈ L) : a ⇨ b ∈ L
• BooleanSubalgebra.val_himp 📋 Mathlib.Order.BooleanSubalgebra
  {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} (a b : ↥L) : ↑(a ⇨ b) = ↑a ⇨ ↑b
• BooleanSubalgebra.mk_himp_mk 📋 Mathlib.Order.BooleanSubalgebra
  {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} (a b : α) (ha : a ∈ L) (hb : b ∈ L) : ⟨a, ha⟩ ⇨ ⟨b, hb⟩ = ⟨a ⇨ b, ⋯⟩
• GeneralizedHeytingAlgebra.copy 📋 Mathlib.Order.Copy
  {α : Type u} (c : GeneralizedHeytingAlgebra α) (le : α → α → Prop) (eq_le : le = LE.le) (top : α) (eq_top : top = ⊤) (sup : α → α → α) (eq_sup : sup = max) (inf : α → α → α) (eq_inf : inf = min) (himp : α → α → α) (eq_himp : himp = HImp.himp) : GeneralizedHeytingAlgebra α
• HeytingAlgebra.copy 📋 Mathlib.Order.Copy
  {α : Type u} (c : HeytingAlgebra α) (le : α → α → Prop) (eq_le : le = LE.le) (top : α) (eq_top : top = ⊤) (bot : α) (eq_bot : bot = ⊥) (sup : α → α → α) (eq_sup : sup = max) (inf : α → α → α) (eq_inf : inf = min) (himp : α → α → α) (eq_himp : himp = HImp.himp) (compl : α → α) (eq_compl : compl = Compl.compl) : HeytingAlgebra α
• BiheytingAlgebra.copy 📋 Mathlib.Order.Copy
  {α : Type u} (c : BiheytingAlgebra α) (le : α → α → Prop) (eq_le : le = LE.le) (top : α) (eq_top : top = ⊤) (bot : α) (eq_bot : bot = ⊥) (sup : α → α → α) (eq_sup : sup = max) (inf : α → α → α) (eq_inf : inf = min) (sdiff : α → α → α) (eq_sdiff : sdiff = SDiff.sdiff) (hnot : α → α) (eq_hnot : hnot = HNot.hnot) (himp : α → α → α) (eq_himp : himp = HImp.himp) (compl : α → α) (eq_compl : compl = Compl.compl) : BiheytingAlgebra α
• Frame.copy 📋 Mathlib.Order.Copy
  {α : Type u} (c : Order.Frame α) (le : α → α → Prop) (eq_le : le = LE.le) (top : α) (eq_top : top = ⊤) (bot : α) (eq_bot : bot = ⊥) (sup : α → α → α) (eq_sup : sup = max) (inf : α → α → α) (eq_inf : inf = min) (himp : α → α → α) (eq_himp : himp = HImp.himp) (compl : α → α) (eq_compl : compl = Compl.compl) (sSup : Set α → α) (eq_sSup : sSup = SupSet.sSup) (sInf : Set α → α) (eq_sInf : sInf = InfSet.sInf) : Order.Frame α
• CompleteDistribLattice.copy 📋 Mathlib.Order.Copy
  {α : Type u} (c : CompleteDistribLattice α) (le : α → α → Prop) (eq_le : le = LE.le) (top : α) (eq_top : top = ⊤) (bot : α) (eq_bot : bot = ⊥) (sup : α → α → α) (eq_sup : sup = max) (inf : α → α → α) (eq_inf : inf = min) (sdiff : α → α → α) (eq_sdiff : sdiff = SDiff.sdiff) (hnot : α → α) (eq_hnot : hnot = HNot.hnot) (himp : α → α → α) (eq_himp : himp = HImp.himp) (compl : α → α) (eq_compl : compl = Compl.compl) (sSup : Set α → α) (eq_sSup : sSup = SupSet.sSup) (sInf : Set α → α) (eq_sInf : sInf = InfSet.sInf) : CompleteDistribLattice α
• TopologicalSpace.Opens.himp_def 📋 Mathlib.Topology.Sets.Opens
  {α : Type u_2} [TopologicalSpace α] {U V : TopologicalSpace.Opens α} : U ⇨ V = TopologicalSpace.Opens.interior (↑U ⇨ ↑V)
• TopologicalSpace.Opens.coe_himp 📋 Mathlib.Topology.Sets.Opens
  {α : Type u_2} [TopologicalSpace α] {U V : TopologicalSpace.Opens α} : ↑(U ⇨ V) = interior (↑U ⇨ ↑V)
• TopologicalSpace.Opens.mem_himp 📋 Mathlib.Topology.Sets.Opens
  {α : Type u_2} [TopologicalSpace α] {U V : TopologicalSpace.Opens α} {x : α} : x ∈ U ⇨ V ↔ ∃ W, W ⊓ U ≤ V ∧ x ∈ W
• TopologicalSpace.Clopens.coe_himp 📋 Mathlib.Topology.Sets.Closeds
  {α : Type u_2} [TopologicalSpace α] (s t : TopologicalSpace.Clopens α) : ↑(s ⇨ t) = ↑s ⇨ ↑t
• TopologicalSpace.CompactOpens.coe_himp 📋 Mathlib.Topology.Sets.Compacts
  {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [T2Space α] (s t : TopologicalSpace.CompactOpens α) : ↑(s ⇨ t) = ↑s ⇨ ↑t
• Topology.IsConstructible.himp 📋 Mathlib.Topology.Constructible
  {X : Type u_2} [TopologicalSpace X] {s t : Set X} : Topology.IsConstructible s → Topology.IsConstructible t → Topology.IsConstructible (s ⇨ t)
• MeasurableSet.himp 📋 Mathlib.MeasureTheory.MeasurableSpace.Defs
  {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) : MeasurableSet (s₁ ⇨ s₂)
• MeasurableSet.coe_himp 📋 Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
  {α : Type u_1} [MeasurableSpace α] (s t : Subtype MeasurableSet) : ↑(s ⇨ t) = ↑s ⇨ ↑t
• SimpleGraph.Finsubgraph.coe_himp 📋 Mathlib.Combinatorics.SimpleGraph.Finsubgraph
  {V : Type u} {G : SimpleGraph V} [Finite V] (G₁ G₂ : G.Finsubgraph) : ↑(G₁ ⇨ G₂) = ↑G₁ ⇨ ↑G₂
• Set.Definable.himp 📋 Mathlib.ModelTheory.Definability
  {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {s t : Set (α → M)} (hs : A.Definable L s) (ht : A.Definable L t) : A.Definable L (s ⇨ t)
• FirstOrder.Language.DefinableSet.coe_himp 📋 Mathlib.ModelTheory.Definability
  {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} (s t : L.DefinableSet A α) : ↑(s ⇨ t) = ↑s ⇨ ↑t
• Heyting.IsRegular.himp 📋 Mathlib.Order.Heyting.Regular
  {α : Type u_1} [HeytingAlgebra α] {a b : α} (ha : Heyting.IsRegular a) (hb : Heyting.IsRegular b) : Heyting.IsRegular (a ⇨ b)
• Heyting.Regular.coe_himp 📋 Mathlib.Order.Heyting.Regular
  {α : Type u_1} [HeytingAlgebra α] (a b : Heyting.Regular α) : ↑(a ⇨ b) = ↑a ⇨ ↑b
• Nucleus.map_himp_le 📋 Mathlib.Order.Nucleus
  {X : Type u_1} [Order.Frame X] {n : Nucleus X} {x y : X} : n (x ⇨ y) ≤ x ⇨ n y
• Nucleus.map_himp_apply 📋 Mathlib.Order.Nucleus
  {X : Type u_1} [Order.Frame X] (n : Nucleus X) (x y : X) : n (x ⇨ n y) = x ⇨ n y
• Nucleus.himp_apply 📋 Mathlib.Order.Nucleus
  {X : Type u_1} [Order.Frame X] (m n : Nucleus X) (x : X) : (m ⇨ n) x = ⨅ y, ⨅ (_ : y ≥ x), m y ⇨ n y
• Sublocale.himp_mem' 📋 Mathlib.Order.Sublocale
  {X : Type u_2} [Order.Frame X] (self : Sublocale X) (a b : X) : b ∈ self.carrier → a ⇨ b ∈ self.carrier
• Sublocale.himp_mem 📋 Mathlib.Order.Sublocale
  {X : Type u_1} [Order.Frame X] {S : Sublocale X} {a b : X} (hb : b ∈ S) : a ⇨ b ∈ S
• Sublocale.mk 📋 Mathlib.Order.Sublocale
  {X : Type u_2} [Order.Frame X] (carrier : Set X) (sInf_mem' : ∀ s ⊆ carrier, sInf s ∈ carrier) (himp_mem' : ∀ (a b : X), b ∈ carrier → a ⇨ b ∈ carrier) : Sublocale X
• Sublocale.mem_mk 📋 Mathlib.Order.Sublocale
  {X : Type u_1} [Order.Frame X] {a : X} (carrier : Set X) (sInf_mem' : ∀ s ⊆ carrier, sInf s ∈ carrier) (himp_mem' : ∀ (a b : X), b ∈ carrier → a ⇨ b ∈ carrier) : a ∈ { carrier := carrier, sInf_mem' := sInf_mem', himp_mem' := himp_mem' } ↔ a ∈ carrier
• Sublocale.coe_himp 📋 Mathlib.Order.Sublocale
  {X : Type u_1} [Order.Frame X] {S : Sublocale X} (a b : ↥S) : ↑(a ⇨ b) = ↑a ⇨ ↑b
• Sublocale.mk_le_mk 📋 Mathlib.Order.Sublocale
  {X : Type u_1} [Order.Frame X] (carrier₁ carrier₂ : Set X) (sInf_mem'₁ : ∀ s ⊆ carrier₁, sInf s ∈ carrier₁) (sInf_mem'₂ : ∀ s ⊆ carrier₂, sInf s ∈ carrier₂) (himp_mem'₁ : ∀ (a b : X), b ∈ carrier₁ → a ⇨ b ∈ carrier₁) (himp_mem'₂ : ∀ (a b : X), b ∈ carrier₂ → a ⇨ b ∈ carrier₂) : { carrier := carrier₁, sInf_mem' := sInf_mem'₁, himp_mem' := himp_mem'₁ } ≤ { carrier := carrier₂, sInf_mem' := sInf_mem'₂, himp_mem' := himp_mem'₂ } ↔ carrier₁ ⊆ carrier₂

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. 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.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c