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 34088
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 34084 . 2 class LHyp
2 vk . . 3 setvar 𝑘
3 cvv 3172 . . 3 class V
4 vx . . . . . 6 setvar 𝑥
54cv 1473 . . . . 5 class 𝑥
62cv 1473 . . . . . 6 class 𝑘
7 cp1 16807 . . . . . 6 class 1.
86, 7cfv 5790 . . . . 5 class (1.‘𝑘)
9 ccvr 33363 . . . . . 6 class
106, 9cfv 5790 . . . . 5 class ( ⋖ ‘𝑘)
115, 8, 10wbr 4577 . . . 4 wff 𝑥( ⋖ ‘𝑘)(1.‘𝑘)
12 cbs 15641 . . . . 5 class Base
136, 12cfv 5790 . . . 4 class (Base‘𝑘)
1411, 4, 13crab 2899 . . 3 class {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)}
152, 3, 14cmpt 4637 . 2 class (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)})
161, 15wceq 1474 1 wff LHyp = (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)})
Colors of variables: wff setvar class
This definition is referenced by:  lhpset  34095
  Copyright terms: Public domain W3C validator