instance Lean.Order.instPreservesSupMeet (a : Prop) : PreservesSup (meet a)

instance Lean.Order.instPreservesSupForallMeet {σ : Type v} {β : σ → Type u} [(s : σ) → CompleteLattice (β s)] [∀ (s : σ) (c : β s), PreservesSup (meet c)] (a : (s : σ) → β s) : PreservesSup (meet a)

noncomputable def Lean.Order.himp {α : Type u} [CompleteLattice α] (a b : α) : α

Heyting implication: the upper adjoint of the lattice meet. For Prop it is →.

Equations

• Lean.Order.himp a b = Lean.Order.PreservesSup.upperAdjoint (Lean.Order.meet a) b

def Lean.Order.«term_⇨_» : TrailingParserDescr

Heyting implication: the upper adjoint of the lattice meet. For Prop it is →.

Equations

• Lean.Order.«term_⇨_» = Lean.ParserDescr.trailingNode `Lean.Order.«term_⇨_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇨ ") (Lean.ParserDescr.cat `term 60))

theorem Lean.Order.le_himp {α : Type u} [CompleteLattice α] {a b x : α} (h : PartialOrder.rel (meet a x) b) : PartialOrder.rel x (himp a b)

Unit for ⇨, the meet specialization of PreservesSup.le_upperAdjoint: a ⊓ x ⊑ b → x ⊑ a ⇨ b.

theorem Lean.Order.meet_himp_le {α : Type u} [CompleteLattice α] {a b : α} [PreservesSup (meet a)] : PartialOrder.rel (meet a (himp a b)) b

Counit for ⇨, the meet specialization of PreservesSup.upperAdjoint_le: a ⊓ (a ⇨ b) ⊑ b.

@[simp]

theorem Lean.Order.himp_prop_eq_imp (a b : Prop) : himp a b = (a → b)

@[simp]

theorem Lean.Order.himp_apply {σ : Type v} {β : Type u} [CompleteLattice β] (a b : σ → β) (s : σ) : himp a b s = himp (a s) (b s)

Pointwise characterization of Heyting implication on function lattices.