Lattice

📁 Source: Mathlib/Algebra/Group/Pointwise/Set/Lattice.lean

Statistics

Metric	Count
Definitions	0
Theorems add_iInter_subset, add_iInter₂_subset, add_iUnion, add_iUnion₂, add_sInter_subset, add_sUnion, div_iInter_subset, div_iInter₂_subset, div_iUnion, div_iUnion₂, div_sInter_subset, div_sUnion, iInter_add_subset, iInter_div_subset, iInter_inv, iInter_mul_subset, iInter_neg, iInter_smul_subset, iInter_sub_subset, iInter_vadd_subset, iInter_vsub_subset, iInter₂_add_subset, iInter₂_div_subset, iInter₂_mul_subset, iInter₂_smul_subset, iInter₂_sub_subset, iInter₂_vadd_subset, iInter₂_vsub_subset, iUnion_add, iUnion_add_left_image, iUnion_add_right_image, iUnion_div, iUnion_div_left_image, iUnion_div_right_image, iUnion_inv, iUnion_mul, iUnion_mul_left_image, iUnion_mul_right_image, iUnion_neg, iUnion_smul, iUnion_smul_left_image, iUnion_smul_right_image, iUnion_smul_set, iUnion_sub, iUnion_sub_left_image, iUnion_sub_right_image, iUnion_vadd, iUnion_vadd_left_image, iUnion_vadd_right_image, iUnion_vadd_set, iUnion_vsub, iUnion_vsub_left_image, iUnion_vsub_right_image, iUnion₂_add, iUnion₂_div, iUnion₂_mul, iUnion₂_smul, iUnion₂_sub, iUnion₂_vadd, iUnion₂_vsub, mul_iInter_subset, mul_iInter₂_subset, mul_iUnion, mul_iUnion₂, mul_sInter_subset, mul_sUnion, sInter_add_subset, sInter_div_subset, sInter_inv, sInter_mul_subset, sInter_neg, sInter_smul_subset, sInter_sub_subset, sInter_vadd_subset, sInter_vsub_subset, sUnion_add, sUnion_div, sUnion_inv, sUnion_mul, sUnion_neg, sUnion_smul, sUnion_sub, sUnion_vadd, sUnion_vsub, smul_iInter_subset, smul_iInter₂_subset, smul_iUnion, smul_iUnion₂, smul_sInter_subset, smul_sUnion, smul_set_iInter_subset, smul_set_iInter₂_subset, smul_set_iUnion, smul_set_iUnion₂, smul_set_sInter_subset, smul_set_sUnion, sub_iInter_subset, sub_iInter₂_subset, sub_iUnion, sub_iUnion₂, sub_sInter_subset, sub_sUnion, vadd_iInter_subset, vadd_iInter₂_subset, vadd_iUnion, vadd_iUnion₂, vadd_sInter_subset, vadd_sUnion, vadd_set_iInter_subset, vadd_set_iInter₂_subset, vadd_set_iUnion, vadd_set_iUnion₂, vadd_set_sInter_subset, vadd_set_sUnion, vsub_iInter_subset, vsub_iInter₂_subset, vsub_iUnion, vsub_iUnion₂, vsub_sInter_subset, vsub_sUnion	120
Total	120

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_iInter_subset 📖	mathematical	—	Set instHasSubset add iInter	—	image2_iInter_subset_right
add_iInter₂_subset 📖	mathematical	—	Set instHasSubset add iInter	—	image2_iInter₂_subset_right
add_iUnion 📖	mathematical	—	Set add iUnion	—	image2_iUnion_right
add_iUnion₂ 📖	mathematical	—	Set add iUnion	—	image2_iUnion₂_right
add_sInter_subset 📖	mathematical	—	Set instHasSubset add sInter iInter instMembership	—	image2_sInter_right_subset
add_sUnion 📖	mathematical	—	Set add sUnion iUnion instMembership	—	image2_sUnion_right
div_iInter_subset 📖	mathematical	—	Set instHasSubset div iInter	—	image2_iInter_subset_right
div_iInter₂_subset 📖	mathematical	—	Set instHasSubset div iInter	—	image2_iInter₂_subset_right
div_iUnion 📖	mathematical	—	Set div iUnion	—	image2_iUnion_right
div_iUnion₂ 📖	mathematical	—	Set div iUnion	—	image2_iUnion₂_right
div_sInter_subset 📖	mathematical	—	Set instHasSubset div sInter iInter instMembership	—	image2_sInter_subset_right
div_sUnion 📖	mathematical	—	Set div sUnion iUnion instMembership	—	image2_sUnion_right
iInter_add_subset 📖	mathematical	—	Set instHasSubset add iInter	—	image2_iInter_subset_left
iInter_div_subset 📖	mathematical	—	Set instHasSubset div iInter	—	image2_iInter_subset_left
iInter_inv 📖	mathematical	—	Set inv iInter	—	preimage_iInter
iInter_mul_subset 📖	mathematical	—	Set instHasSubset mul iInter	—	image2_iInter_subset_left
iInter_neg 📖	mathematical	—	Set neg iInter	—	preimage_iInter
iInter_smul_subset 📖	mathematical	—	Set instHasSubset smul iInter	—	image2_iInter_subset_left
iInter_sub_subset 📖	mathematical	—	Set instHasSubset sub iInter	—	image2_iInter_subset_left
iInter_vadd_subset 📖	mathematical	—	Set instHasSubset HVAdd.hVAdd instHVAdd vadd iInter	—	image2_iInter_subset_left
iInter_vsub_subset 📖	mathematical	—	Set instHasSubset VSub.vsub vsub iInter	—	image2_iInter_subset_left
iInter₂_add_subset 📖	mathematical	—	Set instHasSubset add iInter	—	image2_iInter₂_subset_left
iInter₂_div_subset 📖	mathematical	—	Set instHasSubset div iInter	—	image2_iInter₂_subset_left
iInter₂_mul_subset 📖	mathematical	—	Set instHasSubset mul iInter	—	image2_iInter₂_subset_left
iInter₂_smul_subset 📖	mathematical	—	Set instHasSubset smul iInter	—	image2_iInter₂_subset_left
iInter₂_sub_subset 📖	mathematical	—	Set instHasSubset sub iInter	—	image2_iInter₂_subset_left
iInter₂_vadd_subset 📖	mathematical	—	Set instHasSubset HVAdd.hVAdd instHVAdd vadd iInter	—	image2_iInter₂_subset_left
iInter₂_vsub_subset 📖	mathematical	—	Set instHasSubset VSub.vsub vsub iInter	—	image2_iInter₂_subset_left
iUnion_add 📖	mathematical	—	Set add iUnion	—	image2_iUnion_left
iUnion_add_left_image 📖	mathematical	—	iUnion Set instMembership image add	—	iUnion_image_left
iUnion_add_right_image 📖	mathematical	—	iUnion Set instMembership image add	—	iUnion_image_right
iUnion_div 📖	mathematical	—	Set div iUnion	—	image2_iUnion_left
iUnion_div_left_image 📖	mathematical	—	iUnion Set instMembership image div	—	iUnion_image_left
iUnion_div_right_image 📖	mathematical	—	iUnion Set instMembership image div	—	iUnion_image_right
iUnion_inv 📖	mathematical	—	Set inv iUnion	—	preimage_iUnion
iUnion_mul 📖	mathematical	—	Set mul iUnion	—	image2_iUnion_left
iUnion_mul_left_image 📖	mathematical	—	iUnion Set instMembership image mul	—	iUnion_image_left
iUnion_mul_right_image 📖	mathematical	—	iUnion Set instMembership image mul	—	iUnion_image_right
iUnion_neg 📖	mathematical	—	Set neg iUnion	—	preimage_iUnion
iUnion_smul 📖	mathematical	—	Set smul iUnion	—	image2_iUnion_left
iUnion_smul_left_image 📖	mathematical	—	iUnion Set instMembership smulSet smul	—	iUnion_image_left
iUnion_smul_right_image 📖	mathematical	—	iUnion Set instMembership image smul	—	iUnion_image_right
iUnion_smul_set 📖	mathematical	—	iUnion Set instMembership smulSet smul	—	iUnion_image_left
iUnion_sub 📖	mathematical	—	Set sub iUnion	—	image2_iUnion_left
iUnion_sub_left_image 📖	mathematical	—	iUnion Set instMembership image sub	—	iUnion_image_left
iUnion_sub_right_image 📖	mathematical	—	iUnion Set instMembership image sub	—	iUnion_image_right
iUnion_vadd 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vadd iUnion	—	image2_iUnion_left
iUnion_vadd_left_image 📖	mathematical	—	iUnion Set instMembership HVAdd.hVAdd instHVAdd vaddSet vadd	—	iUnion_image_left
iUnion_vadd_right_image 📖	mathematical	—	iUnion Set instMembership image HVAdd.hVAdd instHVAdd vadd	—	iUnion_image_right
iUnion_vadd_set 📖	mathematical	—	iUnion Set instMembership HVAdd.hVAdd instHVAdd vaddSet vadd	—	iUnion_image_left
iUnion_vsub 📖	mathematical	—	VSub.vsub Set vsub iUnion	—	image2_iUnion_left
iUnion_vsub_left_image 📖	mathematical	—	iUnion Set instMembership image VSub.vsub vsub	—	iUnion_image_left
iUnion_vsub_right_image 📖	mathematical	—	iUnion Set instMembership image VSub.vsub vsub	—	iUnion_image_right
iUnion₂_add 📖	mathematical	—	Set add iUnion	—	image2_iUnion₂_left
iUnion₂_div 📖	mathematical	—	Set div iUnion	—	image2_iUnion₂_left
iUnion₂_mul 📖	mathematical	—	Set mul iUnion	—	image2_iUnion₂_left
iUnion₂_smul 📖	mathematical	—	Set smul iUnion	—	image2_iUnion₂_left
iUnion₂_sub 📖	mathematical	—	Set sub iUnion	—	image2_iUnion₂_left
iUnion₂_vadd 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vadd iUnion	—	image2_iUnion₂_left
iUnion₂_vsub 📖	mathematical	—	VSub.vsub Set vsub iUnion	—	image2_iUnion₂_left
mul_iInter_subset 📖	mathematical	—	Set instHasSubset mul iInter	—	image2_iInter_subset_right
mul_iInter₂_subset 📖	mathematical	—	Set instHasSubset mul iInter	—	image2_iInter₂_subset_right
mul_iUnion 📖	mathematical	—	Set mul iUnion	—	image2_iUnion_right
mul_iUnion₂ 📖	mathematical	—	Set mul iUnion	—	image2_iUnion₂_right
mul_sInter_subset 📖	mathematical	—	Set instHasSubset mul sInter iInter instMembership	—	image2_sInter_right_subset
mul_sUnion 📖	mathematical	—	Set mul sUnion iUnion instMembership	—	image2_sUnion_right
sInter_add_subset 📖	mathematical	—	Set instHasSubset add sInter iInter instMembership	—	image2_sInter_left_subset
sInter_div_subset 📖	mathematical	—	Set instHasSubset div sInter iInter instMembership	—	image2_sInter_subset_left
sInter_inv 📖	mathematical	—	Set inv sInter iInter instMembership	—	preimage_sInter
sInter_mul_subset 📖	mathematical	—	Set instHasSubset mul sInter iInter instMembership	—	image2_sInter_left_subset
sInter_neg 📖	mathematical	—	Set neg sInter iInter instMembership	—	preimage_sInter
sInter_smul_subset 📖	mathematical	—	Set instHasSubset smul sInter iInter instMembership	—	image2_sInter_left_subset
sInter_sub_subset 📖	mathematical	—	Set instHasSubset sub sInter iInter instMembership	—	image2_sInter_subset_left
sInter_vadd_subset 📖	mathematical	—	Set instHasSubset HVAdd.hVAdd instHVAdd vadd sInter iInter instMembership	—	image2_sInter_left_subset
sInter_vsub_subset 📖	mathematical	—	Set instHasSubset VSub.vsub vsub sInter iInter instMembership	—	image2_sInter_subset_left
sUnion_add 📖	mathematical	—	Set add sUnion iUnion instMembership	—	image2_sUnion_left
sUnion_div 📖	mathematical	—	Set div sUnion iUnion instMembership	—	image2_sUnion_left
sUnion_inv 📖	mathematical	—	Set inv sUnion iUnion instMembership	—	preimage_sUnion
sUnion_mul 📖	mathematical	—	Set mul sUnion iUnion instMembership	—	image2_sUnion_left
sUnion_neg 📖	mathematical	—	Set neg sUnion iUnion instMembership	—	preimage_sUnion
sUnion_smul 📖	mathematical	—	Set smul sUnion iUnion instMembership	—	image2_sUnion_left
sUnion_sub 📖	mathematical	—	Set sub sUnion iUnion instMembership	—	image2_sUnion_left
sUnion_vadd 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vadd sUnion iUnion instMembership	—	image2_sUnion_left
sUnion_vsub 📖	mathematical	—	VSub.vsub Set vsub sUnion iUnion instMembership	—	image2_sUnion_left
smul_iInter_subset 📖	mathematical	—	Set instHasSubset smul iInter	—	image2_iInter_subset_right
smul_iInter₂_subset 📖	mathematical	—	Set instHasSubset smul iInter	—	image2_iInter₂_subset_right
smul_iUnion 📖	mathematical	—	Set smul iUnion	—	image2_iUnion_right
smul_iUnion₂ 📖	mathematical	—	Set smul iUnion	—	image2_iUnion₂_right
smul_sInter_subset 📖	mathematical	—	Set instHasSubset smul sInter iInter instMembership	—	image2_sInter_right_subset
smul_sUnion 📖	mathematical	—	Set smul sUnion iUnion instMembership	—	image2_sUnion_right
smul_set_iInter_subset 📖	mathematical	—	Set instHasSubset smulSet iInter	—	image_iInter_subset
smul_set_iInter₂_subset 📖	mathematical	—	Set instHasSubset smulSet iInter	—	image_iInter₂_subset
smul_set_iUnion 📖	mathematical	—	Set smulSet iUnion	—	image_iUnion
smul_set_iUnion₂ 📖	mathematical	—	Set smulSet iUnion	—	image_iUnion₂
smul_set_sInter_subset 📖	mathematical	—	Set instHasSubset smulSet sInter iInter instMembership	—	image_sInter_subset
smul_set_sUnion 📖	mathematical	—	Set smulSet sUnion iUnion instMembership	—	sUnion_eq_biUnion smul_set_iUnion₂
sub_iInter_subset 📖	mathematical	—	Set instHasSubset sub iInter	—	image2_iInter_subset_right
sub_iInter₂_subset 📖	mathematical	—	Set instHasSubset sub iInter	—	image2_iInter₂_subset_right
sub_iUnion 📖	mathematical	—	Set sub iUnion	—	image2_iUnion_right
sub_iUnion₂ 📖	mathematical	—	Set sub iUnion	—	image2_iUnion₂_right
sub_sInter_subset 📖	mathematical	—	Set instHasSubset sub sInter iInter instMembership	—	image2_sInter_subset_right
sub_sUnion 📖	mathematical	—	Set sub sUnion iUnion instMembership	—	image2_sUnion_right
vadd_iInter_subset 📖	mathematical	—	Set instHasSubset HVAdd.hVAdd instHVAdd vadd iInter	—	image2_iInter_subset_right
vadd_iInter₂_subset 📖	mathematical	—	Set instHasSubset HVAdd.hVAdd instHVAdd vadd iInter	—	image2_iInter₂_subset_right
vadd_iUnion 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vadd iUnion	—	image2_iUnion_right
vadd_iUnion₂ 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vadd iUnion	—	image2_iUnion₂_right
vadd_sInter_subset 📖	mathematical	—	Set instHasSubset HVAdd.hVAdd instHVAdd vadd sInter iInter instMembership	—	image2_sInter_right_subset
vadd_sUnion 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vadd sUnion iUnion instMembership	—	image2_sUnion_right
vadd_set_iInter_subset 📖	mathematical	—	Set instHasSubset HVAdd.hVAdd instHVAdd vaddSet iInter	—	image_iInter_subset
vadd_set_iInter₂_subset 📖	mathematical	—	Set instHasSubset HVAdd.hVAdd instHVAdd vaddSet iInter	—	image_iInter₂_subset
vadd_set_iUnion 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vaddSet iUnion	—	image_iUnion
vadd_set_iUnion₂ 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vaddSet iUnion	—	image_iUnion₂
vadd_set_sInter_subset 📖	mathematical	—	Set instHasSubset HVAdd.hVAdd instHVAdd vaddSet sInter iInter instMembership	—	image_sInter_subset
vadd_set_sUnion 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vaddSet sUnion iUnion instMembership	—	sUnion_eq_biUnion vadd_set_iUnion₂
vsub_iInter_subset 📖	mathematical	—	Set instHasSubset VSub.vsub vsub iInter	—	image2_iInter_subset_right
vsub_iInter₂_subset 📖	mathematical	—	Set instHasSubset VSub.vsub vsub iInter	—	image2_iInter₂_subset_right
vsub_iUnion 📖	mathematical	—	VSub.vsub Set vsub iUnion	—	image2_iUnion_right
vsub_iUnion₂ 📖	mathematical	—	VSub.vsub Set vsub iUnion	—	image2_iUnion₂_right
vsub_sInter_subset 📖	mathematical	—	Set instHasSubset VSub.vsub vsub sInter iInter instMembership	—	image2_sInter_subset_right
vsub_sUnion 📖	mathematical	—	VSub.vsub Set vsub sUnion iUnion instMembership	—	image2_sUnion_right

---

← Back to Index