Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lhyp Structured version   Visualization version   GIF version

Definition df-lhyp 37744
Description: Define the set of lattice hyperplanes, which are all lattice elements covered by 1 (i.e., all co-atoms). We call them "hyperplanes" instead of "co-atoms" in analogy with projective geometry hyperplanes. (Contributed by NM, 11-May-2012.)
Assertion
Ref Expression
df-lhyp LHyp = (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)})
Distinct variable group:   𝑥,𝑘

Detailed syntax breakdown of Definition df-lhyp
StepHypRef Expression
1 clh 37740 . 2 class LHyp
2 vk . . 3 setvar 𝑘
3 cvv 3413 . . 3 class V
4 vx . . . . . 6 setvar 𝑥
54cv 1542 . . . . 5 class 𝑥
62cv 1542 . . . . . 6 class 𝑘
7 cp1 17935 . . . . . 6 class 1.
86, 7cfv 6385 . . . . 5 class (1.‘𝑘)
9 ccvr 37018 . . . . . 6 class
106, 9cfv 6385 . . . . 5 class ( ⋖ ‘𝑘)
115, 8, 10wbr 5058 . . . 4 wff 𝑥( ⋖ ‘𝑘)(1.‘𝑘)
12 cbs 16765 . . . . 5 class Base
136, 12cfv 6385 . . . 4 class (Base‘𝑘)
1411, 4, 13crab 3065 . . 3 class {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)}
152, 3, 14cmpt 5140 . 2 class (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)})
161, 15wceq 1543 1 wff LHyp = (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)})
Colors of variables: wff setvar class
This definition is referenced by:  lhpset  37751
  Copyright terms: Public domain W3C validator