SMulAntidiagonal

📁 Source: Mathlib/Data/Finset/SMulAntidiagonal.lean

Statistics

Metric	Count
Definitions SMulAntidiagonal, VAddAntidiagonal	2
Theorems isPWO_support_smulAntidiagonal, isPWO_support_vaddAntidiagonal, mem_smulAntidiagonal, mem_vaddAntidiagonal, smulAntidiagonal_min_smul_min, smulAntidiagonal_mono_left, smulAntidiagonal_mono_right, support_smulAntidiagonal_subset_smul, support_vaddAntidiagonal_subset_vadd, vaddAntidiagonal_min_vadd_min, vaddAntidiagonal_mono_left, vaddAntidiagonal_mono_right, smul, vadd, min_smul, min_vadd, smul, vadd	18
Total	20

Finset

Definitions

Name	Category	Theorems
SMulAntidiagonal 📖	CompOp	6 math math: smulAntidiagonal_mono_right, support_smulAntidiagonal_subset_smul, isPWO_support_smulAntidiagonal, smulAntidiagonal_min_smul_min, smulAntidiagonal_mono_left, mem_smulAntidiagonal
VAddAntidiagonal 📖	CompOp	11 math math: vaddAntidiagonal_mono_left, support_vaddAntidiagonal_subset_vadd, mem_vaddAntidiagonal, HahnSeries.SummableFamily.coeff_smul, isPWO_support_vaddAntidiagonal, HahnModule.coeff_smul, HahnSeries.SummableFamily.sum_vAddAntidiagonal_eq, HahnModule.coeff_smul_left, HahnModule.coeff_smul_right, vaddAntidiagonal_mono_right, vaddAntidiagonal_min_vadd_min

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPWO_support_smulAntidiagonal 📖	mathematical	Set.IsPWO PartialOrder.toPreorder	setOf Nonempty SMulAntidiagonal	—	Set.IsPWO.mono Set.IsPWO.smul IsOrderedCancelSMul.toIsOrderedSMul support_smulAntidiagonal_subset_smul
isPWO_support_vaddAntidiagonal 📖	mathematical	Set.IsPWO PartialOrder.toPreorder	setOf Nonempty VAddAntidiagonal	—	Set.IsPWO.mono Set.IsPWO.vadd IsOrderedCancelVAdd.toIsOrderedVAdd support_vaddAntidiagonal_subset_vadd
mem_smulAntidiagonal 📖	mathematical	Set.IsPWO PartialOrder.toPreorder	Finset instMembership SMulAntidiagonal Set Set.instMembership	—	Set.SMulAntidiagonal.finite_of_isPWO Set.mem_sep_iff
mem_vaddAntidiagonal 📖	mathematical	Set.IsPWO PartialOrder.toPreorder	Finset instMembership VAddAntidiagonal Set Set.instMembership HVAdd.hVAdd instHVAdd	—	Set.VAddAntidiagonal.finite_of_isPWO Set.Finite.mem_toFinset Set.mem_sep_iff
smulAntidiagonal_min_smul_min 📖	mathematical	Set.IsWF Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	SMulAntidiagonal Set.IsWF.isPWO Set.IsWF.min Finset instSingleton	—	ext Set.IsWF.isPWO IsCancelSMul.left_cancel instIsCancelSMulOfIsOrderedCancelSMul LE.le.eq_of_not_lt Set.IsWF.min_le LT.lt.ne' SMul.smul_lt_smul_of_lt_of_le Set.IsWF.min_mem
smulAntidiagonal_mono_left 📖	mathematical	Set.IsPWO PartialOrder.toPreorder Set Set.instHasSubset	Finset instHasSubset SMulAntidiagonal	—	Set.Finite.toFinset_mono Set.SMulAntidiagonal.finite_of_isPWO Set.smulAntidiagonal_mono_left
smulAntidiagonal_mono_right 📖	mathematical	Set.IsPWO PartialOrder.toPreorder Set Set.instHasSubset	Finset instHasSubset SMulAntidiagonal	—	Set.Finite.toFinset_mono Set.SMulAntidiagonal.finite_of_isPWO Set.smulAntidiagonal_mono_right
support_smulAntidiagonal_subset_smul 📖	mathematical	Set.IsPWO PartialOrder.toPreorder	Set Set.instHasSubset setOf Nonempty SMulAntidiagonal Set.smul	—	Set.mem_smul mem_smulAntidiagonal
support_vaddAntidiagonal_subset_vadd 📖	mathematical	Set.IsPWO PartialOrder.toPreorder	Set Set.instHasSubset setOf Nonempty VAddAntidiagonal HVAdd.hVAdd instHVAdd Set.vadd	—	Set.mem_vadd mem_vaddAntidiagonal
vaddAntidiagonal_min_vadd_min 📖	mathematical	Set.IsWF Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	VAddAntidiagonal Set.IsWF.isPWO HVAdd.hVAdd instHVAdd Set.IsWF.min Finset instSingleton	—	ext Set.IsWF.isPWO mem_vaddAntidiagonal mem_singleton IsCancelVAdd.left_cancel instIsCancelVAddOfIsOrderedCancelVAdd LE.le.eq_of_not_lt Set.IsWF.min_le LT.lt.ne' VAdd.vadd_lt_vadd_of_lt_of_le Set.IsWF.min_mem
vaddAntidiagonal_mono_left 📖	mathematical	Set.IsPWO PartialOrder.toPreorder Set Set.instHasSubset	Finset instHasSubset VAddAntidiagonal	—	Set.Finite.toFinset_mono Set.VAddAntidiagonal.finite_of_isPWO Set.vaddAntidiagonal_mono_left
vaddAntidiagonal_mono_right 📖	mathematical	Set.IsPWO PartialOrder.toPreorder Set Set.instHasSubset	Finset instHasSubset VAddAntidiagonal	—	Set.Finite.toFinset_mono Set.VAddAntidiagonal.finite_of_isPWO Set.vaddAntidiagonal_mono_right

Set.IsPWO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul 📖	mathematical	Set.IsPWO	Set Set.smul	—	Set.image_smul_prod image_of_monotone prod Monotone.smul monotone_fst monotone_snd
vadd 📖	mathematical	Set.IsPWO	HVAdd.hVAdd Set instHVAdd Set.vadd	—	Set.vadd_image_prod image_of_monotone prod Monotone.vadd monotone_fst monotone_snd

Set.IsWF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
min_smul 📖	mathematical	Set.IsWF Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	min Set Set.smul smul Set.Nonempty.smul	—	le_antisymm smul Set.Nonempty.smul min_le Set.mem_smul min_mem le_min_iff IsOrderedSMul.smul_le_smul
min_vadd 📖	mathematical	Set.IsWF Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	min HVAdd.hVAdd Set instHVAdd Set.vadd vadd Set.Nonempty.vadd	—	le_antisymm vadd Set.Nonempty.vadd min_le Set.mem_vadd min_mem le_min_iff IsOrderedVAdd.vadd_le_vadd
smul 📖	mathematical	Set.IsWF Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Set.smul	—	Set.IsPWO.isWF Set.IsPWO.smul isPWO
vadd 📖	mathematical	Set.IsWF Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	HVAdd.hVAdd Set instHVAdd Set.vadd	—	Set.IsPWO.isWF Set.IsPWO.vadd isPWO

---

← Back to Index