df-lb - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-lb		Structured version Visualization version GIF version

Definition df-lb 31153

Description: Define the lower bound relationship functor. See brlb 31232 for value. (Contributed by Scott Fenton, 3-May-2018.)

**Assertion**
Ref	Expression
df-lb	⊢ LB𝑅 = UB^◡𝑅

**Detailed syntax breakdown of Definition df-lb**
Step	Hyp	Ref	Expression
1		cR	. . 3 class 𝑅
2	1	clb 31129	. 2 class LB𝑅
3	1	ccnv 5037	. . 3 class ^◡𝑅
4	3	cub 31128	. 2 class UB^◡𝑅
5	2, 4	wceq 1475	1 wff LB𝑅 = UB^◡𝑅

Colors of variables: wff setvar class

This definition is referenced by: brlb 31232