Step
*
of Lemma
order-preserving-map-lattice-lemma
No Annotations
∀[l1,l2:Lattice]. ∀[f:Point(l1) ⟶ Point(l2)].
(∀a,b:Point(l1). f a ∧ b ≤ f a ∧ f b) ∧ (∀a,b:Point(l1). f a ∨ f b ≤ f a ∨ b)
supposing ∀x,y:Point(l1). (x ≤ y
⇒ f x ≤ f y)
BY
{ Auto }
1
1. l1 : Lattice
2. l2 : Lattice
3. f : Point(l1) ⟶ Point(l2)
4. ∀x,y:Point(l1). (x ≤ y
⇒ f x ≤ f y)
5. a : Point(l1)@i
6. b : Point(l1)@i
⊢ f a ∧ b ≤ f a ∧ f b
2
1. l1 : Lattice
2. l2 : Lattice
3. f : Point(l1) ⟶ Point(l2)
4. ∀x,y:Point(l1). (x ≤ y
⇒ f x ≤ f y)
5. ∀a,b:Point(l1). f a ∧ b ≤ f a ∧ f b
6. a : Point(l1)@i
7. b : Point(l1)@i
⊢ f a ∨ f b ≤ f a ∨ b
Latex:
Latex:
No Annotations
\mforall{}[l1,l2:Lattice]. \mforall{}[f:Point(l1) {}\mrightarrow{} Point(l2)].
(\mforall{}a,b:Point(l1). f a \mwedge{} b \mleq{} f a \mwedge{} f b) \mwedge{} (\mforall{}a,b:Point(l1). f a \mvee{} f b \mleq{} f a \mvee{} b)
supposing \mforall{}x,y:Point(l1). (x \mleq{} y {}\mRightarrow{} f x \mleq{} f y)
By
Latex:
Auto
Home
Index