Heyting implication of lower sets

[UPSTREAM] Lower sets of a preorder form a completely distributive lattice, hence a Heyting algebra, in mathlib. This file characterizes membership in the Heyting implication: a lies in P ⇨ Q when every element below a that lies in P lies in Q. This is the support clause of intuitionistic and inquisitive implication, whose propositions are lower sets of information states.

Main results

• LowerSet.mem_himp: membership in P ⇨ Q.

theorem LowerSet.mem_himp {α : Type u_1} [Preorder α] {P Q : LowerSet α} {a : α} : a ∈ P ⇨ Q ↔ ∀ b ≤ a, b ∈ P → b ∈ Q