Documentation

Std.Internal.Order.Lemmas

Complete lattice algebra #

The laws of ⊤, ⊥, ⊓, ⊔, ⨅ and ⨆, their pointwise characterizations on function lattices, and the laws of the Prop lattice.

source
theorem Lean.Order.le_top {α : Type uₗ} [CompleteLattice α] (x : α) :
PartialOrder.rel x top
source
theorem Lean.Order.meet_le_left {α : Type uₗ} [CompleteLattice α] (x y : α) :
PartialOrder.rel (meet x y) x
source
theorem Lean.Order.meet_le_right {α : Type uₗ} [CompleteLattice α] (x y : α) :
PartialOrder.rel (meet x y) y
source
theorem Lean.Order.le_meet {α : Type uₗ} [CompleteLattice α] (x y z : α) :
PartialOrder.rel x y → PartialOrder.rel x z → PartialOrder.rel x (meet y z)
source
theorem Lean.Order.left_le_join {α : Type uₗ} [CompleteLattice α] (x y : α) :
PartialOrder.rel x (join x y)
source
theorem Lean.Order.right_le_join {α : Type uₗ} [CompleteLattice α] (x y : α) :
PartialOrder.rel y (join x y)
source
theorem Lean.Order.join_le {α : Type uₗ} [CompleteLattice α] (x y z : α) :
PartialOrder.rel x z → PartialOrder.rel y z → PartialOrder.rel (join x y) z
source
theorem Lean.Order.iInf_le {α : Type uₗ} [CompleteLattice α] {ι : Type vₗ} (f : ι → α) (i : ι) :
PartialOrder.rel (iInf f) (f i)
source
theorem Lean.Order.le_iInf {α : Type uₗ} [CompleteLattice α] {ι : Type vₗ} (f : ι → α) (x : α) :
(∀ (i : ι), PartialOrder.rel x (f i)) → PartialOrder.rel x (iInf f)
source
@[simp]
theorem Lean.Order.iInf_apply {ι : Type vₗ} {σ : Type wₗ} {β : Type uₗ} [CompleteLattice β] (f : ι → σ → β) (s : σ) :
iInf f s = iInf fun (i : ι) => f i s

Pointwise characterization of indexed infimum on function lattices.

source
theorem Lean.Order.le_iSup {α : Type uₗ} [CompleteLattice α] {ι : Type vₗ} (f : ι → α) (i : ι) :
PartialOrder.rel (f i) (iSup f)
source
theorem Lean.Order.iSup_le {α : Type uₗ} [CompleteLattice α] {ι : Type vₗ} (f : ι → α) (x : α) :
(∀ (i : ι), PartialOrder.rel (f i) x) → PartialOrder.rel (iSup f) x
source
@[simp]
theorem Lean.Order.iSup_apply {ι : Type vₗ} {σ : Type wₗ} {β : Type uₗ} [CompleteLattice β] (f : ι → σ → β) (s : σ) :
iSup f s = iSup fun (i : ι) => f i s

Pointwise characterization of indexed supremum on function lattices.

source
theorem Lean.Order.sup_apply {σ : Type vₗ} {β : σ → Type wₗ} [(s : σ) → CompleteLattice (β s)] (c : ((s : σ) → β s) → Prop) (s : σ) :
CompleteLattice.sup c s = CompleteLattice.sup fun (y : β s) => ∃ (f : (s : σ) → β s), c f ∧ f s = y

Pointwise characterization of CompleteLattice.sup on function lattices: (sup c) s = sup (fun y => ∃ f, c f ∧ f s = y).

source
@[simp]
theorem Lean.Order.meet_apply {σ : Type vₗ} {β : σ → Type wₗ} [(s : σ) → CompleteLattice (β s)] (a b : (s : σ) → β s) (s : σ) :
meet a b s = meet (a s) (b s)

Pointwise characterization of binary meet on function lattices.

source
@[simp]
theorem Lean.Order.join_apply {σ : Type vₗ} {β : Type wₗ} [CompleteLattice β] (a b : σ → β) (s : σ) :
join a b s = join (a s) (b s)

Pointwise characterization of binary join on function lattices.

source
@[simp]
theorem Lean.Order.top_apply {σ : Type vₗ} {β : Type wₗ} [CompleteLattice β] (s : σ) :
top s = top

Pointwise characterization of ⊤ on a function lattice.

source
@[simp]
theorem Lean.Order.bot_apply {σ : Type vₗ} {β : Type wₗ} [CCPO β] (s : σ) :
bot s = bot

Pointwise characterization of ⊥ on a function lattice.

source
@[simp]
theorem Lean.Order.le_prop_eq_imp (p q : Prop) :
PartialOrder.rel p q = (p → q)
source
theorem Lean.Order.le_pi_eq_forall {σ : Type vₗ} {β : σ → Type wₗ} [(s : σ) → PartialOrder (β s)] (a b : (s : σ) → β s) :
PartialOrder.rel a b = ∀ (s : σ), PartialOrder.rel (a s) (b s)

Entailment on a function lattice is pointwise. β is recoverable from the operands' types, so unlike a carrier-only parameter this is a usable @[grind =] trigger; it lets grind push ⊑ through a state argument down to the base lattice.

source
theorem Lean.Order.le_of_imp_top_le (x y : Prop) :
(x → PartialOrder.rel top y) → PartialOrder.rel x y
source
theorem Lean.Order.top_le_prop (x : Prop) :
x → PartialOrder.rel top x
source
theorem Lean.Order.le_of_right (x y : Prop) :
y → PartialOrder.rel x y
source
theorem Lean.Order.of_top_le_prop {x : Prop} :
PartialOrder.rel top x → x
source
theorem Lean.Order.true_le_of_top_le (x : Prop) :
PartialOrder.rel top x → PartialOrder.rel True x
source
@[simp]
theorem Lean.Order.iInf_prop_eq_forall {ι : Type uₗ} (f : ι → Prop) :
iInf f = ∀ (i : ι), f i
source
theorem Lean.Order.le_forall {β : Sort uₗ} (p : Prop) (q : β → Prop) (h : ∀ (x : β), PartialOrder.rel p (q x)) :
PartialOrder.rel p (∀ (x : β), q x)

Introduction rule for a ∀ on the RHS of a Prop entailment.

source
@[simp]
theorem Lean.Order.iSup_prop_eq_exists {ι : Type uₗ} (f : ι → Prop) :
iSup f = ∃ (i : ι), f i
source
@[simp]
theorem Lean.Order.meet_prop_eq_and (a b : Prop) :
meet a b = (a ∧ b)
source
@[simp]
theorem Lean.Order.join_prop_eq_or (a b : Prop) :
join a b = (a ∨ b)
source
theorem Lean.Order.le_iff_forall_le {σ : Type uₗ} {β : Type vₗ} [PartialOrder β] {f g : σ → β} :
PartialOrder.rel f g ↔ ∀ (s : σ), PartialOrder.rel (f s) (g s)

Entailment between functions is pointwise.

source
theorem Lean.Order.le_of_forall_le {σ : Type uₗ} {β : Type vₗ} [PartialOrder β] {f g : σ → β} :
(∀ (s : σ), PartialOrder.rel (f s) (g s)) → PartialOrder.rel f g

Entailment between functions follows from pointwise entailment.

source
theorem Lean.Order.top_le_of_forall_top_le {σ : Type uₗ} {β : Type vₗ} [CompleteLattice β] {g : σ → β} :
(∀ (s : σ), PartialOrder.rel top (g s)) → PartialOrder.rel top g

⊤ ⊑ g for a function g follows from pointwise ⊤ ⊑ g s.

source
@[simp]
theorem Lean.Order.top_prop_eq :
top = True

The top element of the Prop lattice is True.

source
@[simp]
theorem Lean.Order.bot_prop_eq :
bot = False

The bottom element of the Prop lattice is False.

Derived laws of CompleteLattice #

Lattice algebra derived from the laws of CompleteLattice: monotonicity of the connectives, the monoid laws of ⊓ and ⊔ with their units ⊤ and ⊥, and the pointwise unfoldings of ⊑ on function lattices.

Connectives #

source
theorem Lean.Order.le_meet_left {l : Type uₗ} [CompleteLattice l] {P Q : l} (h : PartialOrder.rel P Q) :
PartialOrder.rel P (meet Q P)
source
theorem Lean.Order.le_meet_right {l : Type uₗ} [CompleteLattice l] {P Q : l} (h : PartialOrder.rel P Q) :
PartialOrder.rel P (meet P Q)
source
theorem Lean.Order.le_meet_of_eq {l : Type uₗ} [CompleteLattice l] {P Q R T : l} (hand : T = meet Q R) (hQ : PartialOrder.rel P Q) (hR : PartialOrder.rel P R) :
PartialOrder.rel P T
source
theorem Lean.Order.meet_le_of_left_le {l : Type uₗ} [CompleteLattice l] {P Q R : l} (h : PartialOrder.rel P R) :
PartialOrder.rel (meet P Q) R
source
theorem Lean.Order.meet_le_of_right_le {l : Type uₗ} [CompleteLattice l] {P Q R : l} (h : PartialOrder.rel Q R) :
PartialOrder.rel (meet P Q) R
source
theorem Lean.Order.le_join_of_le_left {l : Type uₗ} [CompleteLattice l] {P Q R : l} (h : PartialOrder.rel P Q) :
PartialOrder.rel P (join Q R)
source
theorem Lean.Order.le_join_of_le_right {l : Type uₗ} [CompleteLattice l] {P Q R : l} (h : PartialOrder.rel P R) :
PartialOrder.rel P (join Q R)
source
theorem Lean.Order.meet_le_comm {l : Type uₗ} [CompleteLattice l] {P Q : l} :
PartialOrder.rel (meet P Q) (meet Q P)
source
theorem Lean.Order.join_le_comm {l : Type uₗ} [CompleteLattice l] {P Q : l} :
PartialOrder.rel (join P Q) (join Q P)
source
theorem Lean.Order.le_trans_meet {l : Type uₗ} [CompleteLattice l] {P Q R : l} (h₁ : PartialOrder.rel P Q) (h₂ : PartialOrder.rel (meet P Q) R) :
PartialOrder.rel P R
source
theorem Lean.Order.le_iSup_of_le {l : Type uₗ} [CompleteLattice l] {P : l} {β : Type u_1} {Ψ : β → l} (a : β) (h : PartialOrder.rel P (Ψ a)) :
PartialOrder.rel P (iSup Ψ)
source
theorem Lean.Order.le_of_le_bot {l : Type uₗ} [CompleteLattice l] {P Q : l} (h : PartialOrder.rel P bot) :
PartialOrder.rel P Q

Monotonicity #

source
theorem Lean.Order.meet_mono {l : Type uₗ} [CompleteLattice l] {P P' Q Q' : l} (hp : PartialOrder.rel P P') (hq : PartialOrder.rel Q Q') :
PartialOrder.rel (meet P Q) (meet P' Q')
source
theorem Lean.Order.meet_mono_left {l : Type uₗ} [CompleteLattice l] {P P' Q : l} (h : PartialOrder.rel P P') :
PartialOrder.rel (meet P Q) (meet P' Q)
source
theorem Lean.Order.meet_mono_right {l : Type uₗ} [CompleteLattice l] {P Q Q' : l} (h : PartialOrder.rel Q Q') :
PartialOrder.rel (meet P Q) (meet P Q')
source
theorem Lean.Order.join_mono {l : Type uₗ} [CompleteLattice l] {P P' Q Q' : l} (hp : PartialOrder.rel P P') (hq : PartialOrder.rel Q Q') :
PartialOrder.rel (join P Q) (join P' Q')
source
theorem Lean.Order.join_mono_left {l : Type uₗ} [CompleteLattice l] {P P' Q : l} (h : PartialOrder.rel P P') :
PartialOrder.rel (join P Q) (join P' Q)
source
theorem Lean.Order.join_mono_right {l : Type uₗ} [CompleteLattice l] {P Q Q' : l} (h : PartialOrder.rel Q Q') :
PartialOrder.rel (join P Q) (join P Q')
source
theorem Lean.Order.iInf_mono {l : Type uₗ} [CompleteLattice l] {β : Type u_1} {Φ Ψ : β → l} (h : ∀ (a : β), PartialOrder.rel (Φ a) (Ψ a)) :
PartialOrder.rel (iInf Φ) (iInf Ψ)
source
theorem Lean.Order.iSup_mono {l : Type uₗ} [CompleteLattice l] {β : Type u_1} {Φ Ψ : β → l} (h : ∀ (a : β), PartialOrder.rel (Φ a) (Ψ a)) :
PartialOrder.rel (iSup Φ) (iSup Ψ)

Boolean algebra #

source
theorem Lean.Order.meet_self {l : Type uₗ} [CompleteLattice l] {P : l} :
meet P P = P
source
theorem Lean.Order.join_self {l : Type uₗ} [CompleteLattice l] {P : l} :
join P P = P
source
theorem Lean.Order.meet_comm {l : Type uₗ} [CompleteLattice l] {P Q : l} :
meet P Q = meet Q P
source
theorem Lean.Order.join_comm {l : Type uₗ} [CompleteLattice l] {P Q : l} :
join P Q = join Q P
source
theorem Lean.Order.meet_assoc {l : Type uₗ} [CompleteLattice l] {P Q R : l} :
meet (meet P Q) R = meet P (meet Q R)
source
theorem Lean.Order.join_assoc {l : Type uₗ} [CompleteLattice l] {P Q R : l} :
join (join P Q) R = join P (join Q R)
source
theorem Lean.Order.le_iff_meet_eq_right {l : Type uₗ} [CompleteLattice l] {P Q : l} :
PartialOrder.rel P Q ↔ meet Q P = P
source
theorem Lean.Order.le_iff_meet_eq_left {l : Type uₗ} [CompleteLattice l] {P Q : l} :
PartialOrder.rel P Q ↔ meet P Q = P
source
theorem Lean.Order.le_iff_join_eq_left {l : Type uₗ} [CompleteLattice l] {P Q : l} :
PartialOrder.rel P Q ↔ join Q P = Q
source
theorem Lean.Order.le_iff_join_eq_right {l : Type uₗ} [CompleteLattice l] {P Q : l} :
PartialOrder.rel P Q ↔ join P Q = Q
source
theorem Lean.Order.top_meet {l : Type uₗ} [CompleteLattice l] {P : l} :
meet top P = P
source
theorem Lean.Order.meet_top {l : Type uₗ} [CompleteLattice l] {P : l} :
meet P top = P
source
theorem Lean.Order.meet_top_le_of_le {l : Type uₗ} [CompleteLattice l] {P Q : l} (h : PartialOrder.rel P Q) :
PartialOrder.rel (meet P top) Q

Cancel a redundant ⊓ ⊤ on the left of an entailment.

source
theorem Lean.Order.bot_meet {l : Type uₗ} [CompleteLattice l] {P : l} :
meet bot P = bot
source
theorem Lean.Order.meet_bot {l : Type uₗ} [CompleteLattice l] {P : l} :
meet P bot = bot
source
theorem Lean.Order.top_join {l : Type uₗ} [CompleteLattice l] {P : l} :
join top P = top
source
theorem Lean.Order.join_top {l : Type uₗ} [CompleteLattice l] {P : l} :
join P top = top
source
theorem Lean.Order.bot_join {l : Type uₗ} [CompleteLattice l] {P : l} :
join bot P = P
source
theorem Lean.Order.join_bot {l : Type uₗ} [CompleteLattice l] {P : l} :
join P bot = P

Miscellaneous #

source
theorem Lean.Order.meet_left_comm {l : Type uₗ} [CompleteLattice l] {P Q R : l} :
meet P (meet Q R) = meet Q (meet P R)
source
theorem Lean.Order.meet_right_comm {l : Type uₗ} [CompleteLattice l] {P Q R : l} :
meet (meet P Q) R = meet (meet P R) Q

Working with entailment #

source
@[simp]
theorem Lean.Order.le_top_iff {l : Type uₗ} [CompleteLattice l] {Q : l} :
PartialOrder.rel Q top ↔ True

Pointwise unfoldings of ⊑ on function lattices #

Fixed-arity instances of le_iff_forall_le for nested function lattices, stated separately per arity so that simp and grind can apply them. Each is definitional via the function-space PartialOrder instance.

source
@[simp]
theorem Lean.Order.le_iff_forall_le_1 {l : Type uₗ} [CompleteLattice l] {σ : Type vₗ} {P Q : σ → l} :
PartialOrder.rel P Q ↔ ∀ (s : σ), PartialOrder.rel (P s) (Q s)
source
@[simp]
theorem Lean.Order.le_iff_forall_le_2 {l : Type uₗ} [CompleteLattice l] {σ₁ σ₂ : Type vₗ} {P Q : σ₁ → σ₂ → l} :
PartialOrder.rel P Q ↔ ∀ (s₁ : σ₁) (s₂ : σ₂), PartialOrder.rel (P s₁ s₂) (Q s₁ s₂)
source
@[simp]
theorem Lean.Order.le_iff_forall_le_3 {l : Type uₗ} [CompleteLattice l] {σ₁ σ₂ σ₃ : Type vₗ} {P Q : σ₁ → σ₂ → σ₃ → l} :
PartialOrder.rel P Q ↔ ∀ (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃), PartialOrder.rel (P s₁ s₂ s₃) (Q s₁ s₂ s₃)
source
@[simp]
theorem Lean.Order.le_iff_forall_le_4 {l : Type uₗ} [CompleteLattice l] {σ₁ σ₂ σ₃ σ₄ : Type vₗ} {P Q : σ₁ → σ₂ → σ₃ → σ₄ → l} :
PartialOrder.rel P Q ↔ ∀ (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) (s₄ : σ₄), PartialOrder.rel (P s₁ s₂ s₃ s₄) (Q s₁ s₂ s₃ s₄)
source
@[simp]
theorem Lean.Order.le_iff_forall_le_5 {l : Type uₗ} [CompleteLattice l] {σ₁ σ₂ σ₃ σ₄ σ₅ : Type vₗ} {P Q : σ₁ → σ₂ → σ₃ → σ₄ → σ₅ → l} :
PartialOrder.rel P Q ↔ ∀ (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) (s₄ : σ₄) (s₅ : σ₅), PartialOrder.rel (P s₁ s₂ s₃ s₄ s₅) (Q s₁ s₂ s₃ s₄ s₅)