Derived laws of CompleteLattice

This module contains some laws about CompleteLattice that are derived from the laws in Std.Internal.Do.CompleteLattice.CompleteLattice.

Connectives

theorem Std.Internal.Do.CompleteLattice.le_meet_left {l : Type u} [Lean.Order.CompleteLattice l] {P Q : l} (h : Lean.Order.PartialOrder.rel P Q) : Lean.Order.PartialOrder.rel P (Lean.Order.meet Q P)

theorem Std.Internal.Do.CompleteLattice.le_meet_right {l : Type u} [Lean.Order.CompleteLattice l] {P Q : l} (h : Lean.Order.PartialOrder.rel P Q) : Lean.Order.PartialOrder.rel P (Lean.Order.meet P Q)

theorem Std.Internal.Do.CompleteLattice.le_meet_of_eq {l : Type u} [Lean.Order.CompleteLattice l] {P Q R T : l} (hand : T = Lean.Order.meet Q R) (hQ : Lean.Order.PartialOrder.rel P Q) (hR : Lean.Order.PartialOrder.rel P R) : Lean.Order.PartialOrder.rel P T

theorem Std.Internal.Do.CompleteLattice.meet_le_of_left_le {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} (h : Lean.Order.PartialOrder.rel P R) : Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) R

theorem Std.Internal.Do.CompleteLattice.meet_le_of_right_le {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} (h : Lean.Order.PartialOrder.rel Q R) : Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) R

theorem Std.Internal.Do.CompleteLattice.le_join_of_le_left {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} (h : Lean.Order.PartialOrder.rel P Q) : Lean.Order.PartialOrder.rel P (Lean.Order.join Q R)

theorem Std.Internal.Do.CompleteLattice.le_join_of_le_right {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} (h : Lean.Order.PartialOrder.rel P R) : Lean.Order.PartialOrder.rel P (Lean.Order.join Q R)

theorem Std.Internal.Do.CompleteLattice.meet_le_comm {l : Type u} [Lean.Order.CompleteLattice l] {P Q : l} : Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) (Lean.Order.meet Q P)

theorem Std.Internal.Do.CompleteLattice.join_le_comm {l : Type u} [Lean.Order.CompleteLattice l] {P Q : l} : Lean.Order.PartialOrder.rel (Lean.Order.join P Q) (Lean.Order.join Q P)

theorem Std.Internal.Do.CompleteLattice.le_trans_meet {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} (h₁ : Lean.Order.PartialOrder.rel P Q) (h₂ : Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) R) : Lean.Order.PartialOrder.rel P R

theorem Std.Internal.Do.CompleteLattice.le_iSup_of_le {l : Type u} [Lean.Order.CompleteLattice l] {P : l} {α : Type u_1} {Ψ : α → l} (a : α) (h : Lean.Order.PartialOrder.rel P (Ψ a)) : Lean.Order.PartialOrder.rel P (Lean.Order.iSup Ψ)

theorem Std.Internal.Do.CompleteLattice.le_of_le_bot {l : Type u} [Lean.Order.CompleteLattice l] {P Q : l} (h : Lean.Order.PartialOrder.rel P Lean.Order.bot) : Lean.Order.PartialOrder.rel P Q

Connectives requiring Frame

theorem Std.Internal.Do.CompleteLattice.le_himp {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} [Lean.Order.Frame l] (h : Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) R) : Lean.Order.PartialOrder.rel P (Lean.Order.himp Q R)

theorem Std.Internal.Do.CompleteLattice.le_himp_of_meet_le_comm {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} [Lean.Order.Frame l] (h : Lean.Order.PartialOrder.rel (Lean.Order.meet Q P) R) : Lean.Order.PartialOrder.rel P (Lean.Order.himp Q R)

theorem Std.Internal.Do.CompleteLattice.meet_le_of_le_himp {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} [Lean.Order.Frame l] (h : Lean.Order.PartialOrder.rel P (Lean.Order.himp Q R)) : Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) R

theorem Std.Internal.Do.CompleteLattice.meet_le_of_le_himp_comm {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} [Lean.Order.Frame l] (h : Lean.Order.PartialOrder.rel Q (Lean.Order.himp P R)) : Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) R

theorem Std.Internal.Do.CompleteLattice.himp_meet_le {l : Type u} [Lean.Order.CompleteLattice l] {P Q : l} [Lean.Order.Frame l] : Lean.Order.PartialOrder.rel (Lean.Order.meet (Lean.Order.himp P Q) P) Q

theorem Std.Internal.Do.CompleteLattice.meet_himp_le {l : Type u} [Lean.Order.CompleteLattice l] {P Q : l} [Lean.Order.Frame l] : Lean.Order.PartialOrder.rel (Lean.Order.meet P (Lean.Order.himp P Q)) Q

theorem Std.Internal.Do.CompleteLattice.le_himp_mp {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} [Lean.Order.Frame l] (h₁ : Lean.Order.PartialOrder.rel P (Lean.Order.himp Q R)) (h₂ : Lean.Order.PartialOrder.rel P Q) : Lean.Order.PartialOrder.rel P R

theorem Std.Internal.Do.CompleteLattice.meet_join_le_left {l : Type u} [Lean.Order.CompleteLattice l] {P Q R T : l} [Lean.Order.Frame l] (hleft : Lean.Order.PartialOrder.rel (Lean.Order.meet P R) T) (hright : Lean.Order.PartialOrder.rel (Lean.Order.meet Q R) T) : Lean.Order.PartialOrder.rel (Lean.Order.meet (Lean.Order.join P Q) R) T

theorem Std.Internal.Do.CompleteLattice.meet_join_le_right {l : Type u} [Lean.Order.CompleteLattice l] {P Q R T : l} [Lean.Order.Frame l] (hleft : Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) T) (hright : Lean.Order.PartialOrder.rel (Lean.Order.meet P R) T) : Lean.Order.PartialOrder.rel (Lean.Order.meet P (Lean.Order.join Q R)) T

Monotonicity

theorem Std.Internal.Do.CompleteLattice.meet_mono {l : Type u} [Lean.Order.CompleteLattice l] {P P' Q Q' : l} (hp : Lean.Order.PartialOrder.rel P P') (hq : Lean.Order.PartialOrder.rel Q Q') : Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) (Lean.Order.meet P' Q')

theorem Std.Internal.Do.CompleteLattice.meet_mono_left {l : Type u} [Lean.Order.CompleteLattice l] {P P' Q : l} (h : Lean.Order.PartialOrder.rel P P') : Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) (Lean.Order.meet P' Q)

theorem Std.Internal.Do.CompleteLattice.meet_mono_right {l : Type u} [Lean.Order.CompleteLattice l] {P Q Q' : l} (h : Lean.Order.PartialOrder.rel Q Q') : Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) (Lean.Order.meet P Q')

theorem Std.Internal.Do.CompleteLattice.join_mono {l : Type u} [Lean.Order.CompleteLattice l] {P P' Q Q' : l} (hp : Lean.Order.PartialOrder.rel P P') (hq : Lean.Order.PartialOrder.rel Q Q') : Lean.Order.PartialOrder.rel (Lean.Order.join P Q) (Lean.Order.join P' Q')

theorem Std.Internal.Do.CompleteLattice.join_mono_left {l : Type u} [Lean.Order.CompleteLattice l] {P P' Q : l} (h : Lean.Order.PartialOrder.rel P P') : Lean.Order.PartialOrder.rel (Lean.Order.join P Q) (Lean.Order.join P' Q)

theorem Std.Internal.Do.CompleteLattice.join_mono_right {l : Type u} [Lean.Order.CompleteLattice l] {P Q Q' : l} (h : Lean.Order.PartialOrder.rel Q Q') : Lean.Order.PartialOrder.rel (Lean.Order.join P Q) (Lean.Order.join P Q')

theorem Std.Internal.Do.CompleteLattice.iInf_mono {l : Type u} [Lean.Order.CompleteLattice l] {α : Type u_1} {Φ Ψ : α → l} (h : ∀ (a : α), Lean.Order.PartialOrder.rel (Φ a) (Ψ a)) : Lean.Order.PartialOrder.rel (Lean.Order.iInf Φ) (Lean.Order.iInf Ψ)

theorem Std.Internal.Do.CompleteLattice.iSup_mono {l : Type u} [Lean.Order.CompleteLattice l] {α : Type u_1} {Φ Ψ : α → l} (h : ∀ (a : α), Lean.Order.PartialOrder.rel (Φ a) (Ψ a)) : Lean.Order.PartialOrder.rel (Lean.Order.iSup Φ) (Lean.Order.iSup Ψ)

theorem Std.Internal.Do.CompleteLattice.himp_mono {l : Type u} [Lean.Order.CompleteLattice l] {P P' Q Q' : l} [Lean.Order.Frame l] (h1 : Lean.Order.PartialOrder.rel Q P) (h2 : Lean.Order.PartialOrder.rel P' Q') : Lean.Order.PartialOrder.rel (Lean.Order.himp P P') (Lean.Order.himp Q Q')

theorem Std.Internal.Do.CompleteLattice.himp_mono_left {l : Type u} [Lean.Order.CompleteLattice l] {P P' Q : l} [Lean.Order.Frame l] (h : Lean.Order.PartialOrder.rel P' P) : Lean.Order.PartialOrder.rel (Lean.Order.himp P Q) (Lean.Order.himp P' Q)

theorem Std.Internal.Do.CompleteLattice.himp_mono_right {l : Type u} [Lean.Order.CompleteLattice l] {P Q Q' : l} [Lean.Order.Frame l] (h : Lean.Order.PartialOrder.rel Q Q') : Lean.Order.PartialOrder.rel (Lean.Order.himp P Q) (Lean.Order.himp P Q')

Boolean algebra

theorem Std.Internal.Do.CompleteLattice.meet_self {l : Type u} [Lean.Order.CompleteLattice l] {P : l} : Lean.Order.meet P P = P

theorem Std.Internal.Do.CompleteLattice.join_self {l : Type u} [Lean.Order.CompleteLattice l] {P : l} : Lean.Order.join P P = P

theorem Std.Internal.Do.CompleteLattice.meet_comm {l : Type u} [Lean.Order.CompleteLattice l] {P Q : l} : Lean.Order.meet P Q = Lean.Order.meet Q P

theorem Std.Internal.Do.CompleteLattice.join_comm {l : Type u} [Lean.Order.CompleteLattice l] {P Q : l} : Lean.Order.join P Q = Lean.Order.join Q P

theorem Std.Internal.Do.CompleteLattice.meet_assoc {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} : Lean.Order.meet (Lean.Order.meet P Q) R = Lean.Order.meet P (Lean.Order.meet Q R)

theorem Std.Internal.Do.CompleteLattice.join_assoc {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} : Lean.Order.join (Lean.Order.join P Q) R = Lean.Order.join P (Lean.Order.join Q R)

theorem Std.Internal.Do.CompleteLattice.le_iff_meet_eq_right {l : Type u} [Lean.Order.CompleteLattice l] {P Q : l} : Lean.Order.PartialOrder.rel P Q ↔ Lean.Order.meet Q P = P

theorem Std.Internal.Do.CompleteLattice.le_iff_meet_eq_left {l : Type u} [Lean.Order.CompleteLattice l] {P Q : l} : Lean.Order.PartialOrder.rel P Q ↔ Lean.Order.meet P Q = P

theorem Std.Internal.Do.CompleteLattice.le_iff_join_eq_left {l : Type u} [Lean.Order.CompleteLattice l] {P Q : l} : Lean.Order.PartialOrder.rel P Q ↔ Lean.Order.join Q P = Q

theorem Std.Internal.Do.CompleteLattice.le_iff_join_eq_right {l : Type u} [Lean.Order.CompleteLattice l] {P Q : l} : Lean.Order.PartialOrder.rel P Q ↔ Lean.Order.join P Q = Q

theorem Std.Internal.Do.CompleteLattice.top_meet {l : Type u} [Lean.Order.CompleteLattice l] {P : l} : Lean.Order.meet Lean.Order.top P = P

theorem Std.Internal.Do.CompleteLattice.meet_top {l : Type u} [Lean.Order.CompleteLattice l] {P : l} : Lean.Order.meet P Lean.Order.top = P

theorem Std.Internal.Do.CompleteLattice.bot_meet {l : Type u} [Lean.Order.CompleteLattice l] {P : l} : Lean.Order.meet Lean.Order.bot P = Lean.Order.bot

theorem Std.Internal.Do.CompleteLattice.meet_bot {l : Type u} [Lean.Order.CompleteLattice l] {P : l} : Lean.Order.meet P Lean.Order.bot = Lean.Order.bot

theorem Std.Internal.Do.CompleteLattice.top_join {l : Type u} [Lean.Order.CompleteLattice l] {P : l} : Lean.Order.join Lean.Order.top P = Lean.Order.top

theorem Std.Internal.Do.CompleteLattice.join_top {l : Type u} [Lean.Order.CompleteLattice l] {P : l} : Lean.Order.join P Lean.Order.top = Lean.Order.top

theorem Std.Internal.Do.CompleteLattice.bot_join {l : Type u} [Lean.Order.CompleteLattice l] {P : l} : Lean.Order.join Lean.Order.bot P = P

theorem Std.Internal.Do.CompleteLattice.join_bot {l : Type u} [Lean.Order.CompleteLattice l] {P : l} : Lean.Order.join P Lean.Order.bot = P

theorem Std.Internal.Do.CompleteLattice.meet_join_left {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} [Lean.Order.Frame l] : Lean.Order.meet P (Lean.Order.join Q R) = Lean.Order.join (Lean.Order.meet P Q) (Lean.Order.meet P R)

theorem Std.Internal.Do.CompleteLattice.join_meet_left {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} [Lean.Order.Frame l] : Lean.Order.join P (Lean.Order.meet Q R) = Lean.Order.meet (Lean.Order.join P Q) (Lean.Order.join P R)

theorem Std.Internal.Do.CompleteLattice.meet_join_right {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} [Lean.Order.Frame l] : Lean.Order.meet (Lean.Order.join P Q) R = Lean.Order.join (Lean.Order.meet P R) (Lean.Order.meet Q R)

theorem Std.Internal.Do.CompleteLattice.join_meet_right {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} [Lean.Order.Frame l] : Lean.Order.join (Lean.Order.meet P Q) R = Lean.Order.meet (Lean.Order.join P R) (Lean.Order.join Q R)

theorem Std.Internal.Do.CompleteLattice.top_himp {l : Type u} [Lean.Order.CompleteLattice l] {P : l} [Lean.Order.Frame l] : Lean.Order.himp Lean.Order.top P = P

theorem Std.Internal.Do.CompleteLattice.le_himp_self {l : Type u} [Lean.Order.CompleteLattice l] {P Q : l} [Lean.Order.Frame l] : Lean.Order.PartialOrder.rel Q (Lean.Order.himp P P)

theorem Std.Internal.Do.CompleteLattice.le_himp_self_iff {l : Type u} [Lean.Order.CompleteLattice l] {P Q : l} [Lean.Order.Frame l] : Lean.Order.PartialOrder.rel Q (Lean.Order.himp P P) ↔ True

theorem Std.Internal.Do.CompleteLattice.himp_meet_himp_le {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} [Lean.Order.Frame l] : Lean.Order.PartialOrder.rel (Lean.Order.meet (Lean.Order.himp P Q) (Lean.Order.himp Q R)) (Lean.Order.himp P R)

theorem Std.Internal.Do.CompleteLattice.bot_himp {l : Type u} [Lean.Order.CompleteLattice l] {P : l} [Lean.Order.Frame l] : Lean.Order.himp Lean.Order.bot P = Lean.Order.top

theorem Std.Internal.Do.CompleteLattice.meet_himp_le_meet {l : Type u} [Lean.Order.CompleteLattice l] {P' Q' : l} [Lean.Order.Frame l] : Lean.Order.PartialOrder.rel (Lean.Order.meet P' (Lean.Order.himp P' Q')) (Lean.Order.meet P' Q')

theorem Std.Internal.Do.CompleteLattice.meet_le_meet_of_le_himp {l : Type u} [Lean.Order.CompleteLattice l] {P P' Q Q' : l} [Lean.Order.Frame l] (hp : Lean.Order.PartialOrder.rel P P') (hq : Lean.Order.PartialOrder.rel Q (Lean.Order.himp P' Q')) : Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) (Lean.Order.meet P' Q')

Propositional embedding (CompleteLattice.ofProp)

theorem Std.Internal.Do.CompleteLattice.ofProp_elim {l : Type u} [Lean.Order.CompleteLattice l] {Q R : l} {φ : Prop} (h1 : Lean.Order.PartialOrder.rel Q (Lean.Order.CompleteLattice.ofProp φ)) (h2 : φ → Lean.Order.PartialOrder.rel Q R) : Lean.Order.PartialOrder.rel Q R

theorem Std.Internal.Do.CompleteLattice.ofProp_mono {l : Type u} [Lean.Order.CompleteLattice l] {φ₁ φ₂ : Prop} (h : φ₁ → φ₂) : Lean.Order.PartialOrder.rel (Lean.Order.CompleteLattice.ofProp φ₁) (Lean.Order.CompleteLattice.ofProp φ₂)

theorem Std.Internal.Do.CompleteLattice.ofProp_congr {l : Type u} [Lean.Order.CompleteLattice l] {φ₁ φ₂ : Prop} (h : φ₁ ↔ φ₂) : Lean.Order.CompleteLattice.ofProp φ₁ = Lean.Order.CompleteLattice.ofProp φ₂

theorem Std.Internal.Do.CompleteLattice.ofProp_meet_le_left {l : Type u} [Lean.Order.CompleteLattice l] {Q R : l} {φ : Prop} (h : φ → Lean.Order.PartialOrder.rel Q R) : Lean.Order.PartialOrder.rel (Lean.Order.meet (Lean.Order.CompleteLattice.ofProp φ) Q) R

theorem Std.Internal.Do.CompleteLattice.ofProp_meet_le_right {l : Type u} [Lean.Order.CompleteLattice l] {Q R : l} {φ : Prop} (h : φ → Lean.Order.PartialOrder.rel Q R) : Lean.Order.PartialOrder.rel (Lean.Order.meet Q (Lean.Order.CompleteLattice.ofProp φ)) R

theorem Std.Internal.Do.CompleteLattice.ofProp_eq_top {l : Type u} [Lean.Order.CompleteLattice l] {φ : Prop} (h : φ) : Lean.Order.CompleteLattice.ofProp φ = Lean.Order.top

theorem Std.Internal.Do.CompleteLattice.ofProp_and {l : Type u} [Lean.Order.CompleteLattice l] {φ₁ φ₂ : Prop} : Lean.Order.meet (Lean.Order.CompleteLattice.ofProp φ₁) (Lean.Order.CompleteLattice.ofProp φ₂) = Lean.Order.CompleteLattice.ofProp (φ₁ ∧ φ₂)

theorem Std.Internal.Do.CompleteLattice.ofProp_or {l : Type u} [Lean.Order.CompleteLattice l] {φ₁ φ₂ : Prop} : Lean.Order.join (Lean.Order.CompleteLattice.ofProp φ₁) (Lean.Order.CompleteLattice.ofProp φ₂) = Lean.Order.CompleteLattice.ofProp (φ₁ ∨ φ₂)

theorem Std.Internal.Do.CompleteLattice.ofProp_forall_le {l : Type u} [Lean.Order.CompleteLattice l] {α : Type u_1} {Φ : α → Prop} : Lean.Order.PartialOrder.rel (Lean.Order.CompleteLattice.ofProp (∀ (x : α), Φ x)) (Lean.Order.iInf fun (x : α) => Lean.Order.CompleteLattice.ofProp (Φ x))

theorem Std.Internal.Do.CompleteLattice.ofProp_exists {l : Type u} [Lean.Order.CompleteLattice l] {α : Type u_1} {Φ : α → Prop} : (Lean.Order.iSup fun (x : α) => Lean.Order.CompleteLattice.ofProp (Φ x)) = Lean.Order.CompleteLattice.ofProp (∃ (x : α), Φ x)

theorem Std.Internal.Do.CompleteLattice.ofProp_forall {l : Type u} [Lean.Order.CompleteLattice l] {α : Type u_1} {Φ : α → Prop} : (Lean.Order.iInf fun (x : α) => Lean.Order.CompleteLattice.ofProp (Φ x)) = Lean.Order.CompleteLattice.ofProp (∀ (x : α), Φ x)

theorem Std.Internal.Do.CompleteLattice.himp_ofProp_le {l : Type u} [Lean.Order.CompleteLattice l] [Lean.Order.Frame l] {φ₁ φ₂ : Prop} : Lean.Order.PartialOrder.rel (Lean.Order.CompleteLattice.ofProp (φ₁ → φ₂)) (Lean.Order.himp (Lean.Order.CompleteLattice.ofProp φ₁) (Lean.Order.CompleteLattice.ofProp φ₂))

theorem Std.Internal.Do.CompleteLattice.himp_ofProp {l : Type u} [Lean.Order.CompleteLattice l] [Lean.Order.Frame l] {φ₁ φ₂ : Prop} : Lean.Order.himp (Lean.Order.CompleteLattice.ofProp φ₁) (Lean.Order.CompleteLattice.ofProp φ₂) = Lean.Order.CompleteLattice.ofProp (φ₁ → φ₂)

Miscellaneous

theorem Std.Internal.Do.CompleteLattice.meet_left_comm {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} : Lean.Order.meet P (Lean.Order.meet Q R) = Lean.Order.meet Q (Lean.Order.meet P R)

theorem Std.Internal.Do.CompleteLattice.meet_right_comm {l : Type u} [Lean.Order.CompleteLattice l] {P Q R : l} : Lean.Order.meet (Lean.Order.meet P Q) R = Lean.Order.meet (Lean.Order.meet P R) Q

Working with entailment

@[simp]

theorem Std.Internal.Do.CompleteLattice.top_le_himp_iff {l : Type u} [Lean.Order.CompleteLattice l] [Lean.Order.Frame l] (P Q : l) : Lean.Order.PartialOrder.rel Lean.Order.top (Lean.Order.himp P Q) ↔ Lean.Order.PartialOrder.rel P Q

⊤ ⊑ (P ⇨ Q) iff P ⊑ Q.

@[simp]

theorem Std.Internal.Do.CompleteLattice.le_top_iff {l : Type u} [Lean.Order.CompleteLattice l] {Q : l} : Lean.Order.PartialOrder.rel Q Lean.Order.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.

@[simp]

theorem Std.Internal.Do.CompleteLattice.le_iff_forall_le_1 {l : Type u} [Lean.Order.CompleteLattice l] {σ : Type v} {P Q : σ → l} : Lean.Order.PartialOrder.rel P Q ↔ ∀ (s : σ), Lean.Order.PartialOrder.rel (P s) (Q s)

@[simp]

theorem Std.Internal.Do.CompleteLattice.le_iff_forall_le_2 {l : Type u} [Lean.Order.CompleteLattice l] {σ₁ σ₂ : Type v} {P Q : σ₁ → σ₂ → l} : Lean.Order.PartialOrder.rel P Q ↔ ∀ (s₁ : σ₁) (s₂ : σ₂), Lean.Order.PartialOrder.rel (P s₁ s₂) (Q s₁ s₂)

@[simp]

theorem Std.Internal.Do.CompleteLattice.le_iff_forall_le_3 {l : Type u} [Lean.Order.CompleteLattice l] {σ₁ σ₂ σ₃ : Type v} {P Q : σ₁ → σ₂ → σ₃ → l} : Lean.Order.PartialOrder.rel P Q ↔ ∀ (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃), Lean.Order.PartialOrder.rel (P s₁ s₂ s₃) (Q s₁ s₂ s₃)

@[simp]

theorem Std.Internal.Do.CompleteLattice.le_iff_forall_le_4 {l : Type u} [Lean.Order.CompleteLattice l] {σ₁ σ₂ σ₃ σ₄ : Type v} {P Q : σ₁ → σ₂ → σ₃ → σ₄ → l} : Lean.Order.PartialOrder.rel P Q ↔ ∀ (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) (s₄ : σ₄), Lean.Order.PartialOrder.rel (P s₁ s₂ s₃ s₄) (Q s₁ s₂ s₃ s₄)

@[simp]

theorem Std.Internal.Do.CompleteLattice.le_iff_forall_le_5 {l : Type u} [Lean.Order.CompleteLattice l] {σ₁ σ₂ σ₃ σ₄ σ₅ : Type v} {P Q : σ₁ → σ₂ → σ₃ → σ₄ → σ₅ → l} : Lean.Order.PartialOrder.rel P Q ↔ ∀ (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) (s₄ : σ₄) (s₅ : σ₅), Lean.Order.PartialOrder.rel (P s₁ s₂ s₃ s₄ s₅) (Q s₁ s₂ s₃ s₄ s₅)