Documentation Verification Report

SMulAntidiagonal

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

Statistics

Metric	Count
Definitions `smulAntidiagonal`, `vaddAntidiagonal`	2
Theorems `eq_of_fst_eq_fst`, `eq_of_fst_le_fst_of_snd_le_snd`, `eq_of_snd_eq_snd`, `finite_of_isPWO`, `fst_eq_fst_iff_snd_eq_snd`, `eq_of_fst_eq_fst`, `eq_of_fst_le_fst_of_snd_le_snd`, `eq_of_snd_eq_snd`, `finite_of_isPWO`, `fst_eq_fst_iff_snd_eq_snd`, `mem_smulAntidiagonal`, `mem_vaddAntidiagonal`, `smulAntidiagonal_mono_left`, `smulAntidiagonal_mono_right`, `vaddAntidiagonal_mono_left`, `vaddAntidiagonal_mono_right`	16
Total	18

Set

Definitions

Name	Category	Theorems
`smulAntidiagonal` 📖	CompOp	5 math math: `smulAntidiagonal_mono_right`, `smulAntidiagonal_mono_left`, `mem_smulAntidiagonal`, `SMulAntidiagonal.finite_of_isPWO`, `SMulAntidiagonal.fst_eq_fst_iff_snd_eq_snd`
`vaddAntidiagonal` 📖	CompOp	6 math math: `vaddAntidiagonal_mono_left`, `VAddAntidiagonal.finite_of_isPWO`, `vaddAntidiagonal_mono_right`, `mem_vaddAntidiagonal`, `Finsupp.finite_vaddAntidiagonal`, `VAddAntidiagonal.fst_eq_fst_iff_snd_eq_snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_smulAntidiagonal` 📖	mathematical	—	`Set` `instMembership` `smulAntidiagonal`	—	—
`mem_vaddAntidiagonal` 📖	mathematical	—	`Set` `instMembership` `vaddAntidiagonal` `HVAdd.hVAdd` `instHVAdd`	—	—
`smulAntidiagonal_mono_left` 📖	mathematical	`Set` `instHasSubset`	`smulAntidiagonal`	—	—
`smulAntidiagonal_mono_right` 📖	mathematical	`Set` `instHasSubset`	`smulAntidiagonal`	—	—
`vaddAntidiagonal_mono_left` 📖	mathematical	`Set` `instHasSubset`	`vaddAntidiagonal`	—	—
`vaddAntidiagonal_mono_right` 📖	mathematical	`Set` `instHasSubset`	`vaddAntidiagonal`	—	—

Set.SMulAntidiagonal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_fst_eq_fst` 📖	—	`Set` `Set.instMembership` `Set.smulAntidiagonal`	—	—	`fst_eq_fst_iff_snd_eq_snd`
`eq_of_fst_le_fst_of_snd_le_snd` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `Set` `Set.instMembership` `Set.smulAntidiagonal`	—	—	`eq_of_fst_eq_fst` `instIsCancelSMulOfIsOrderedCancelSMul` `LE.le.eq_of_not_lt` `LT.lt.ne` `SMul.smul_lt_smul_of_lt_of_le` `Set.mem_smulAntidiagonal`
`eq_of_snd_eq_snd` 📖	—	`Set` `Set.instMembership` `Set.smulAntidiagonal`	—	—	`fst_eq_fst_iff_snd_eq_snd`
`finite_of_isPWO` 📖	mathematical	`Set.IsPWO` `PartialOrder.toPreorder`	`Set.Finite` `Set.smulAntidiagonal`	—	`Set.mem_smulAntidiagonal` `Set.PartiallyWellOrderedOn.exists_monotone_subseq` `Order.Preimage.instIsPreorder` `instIsPreorderLe` `LT.lt.ne` `RelEmbedding.injective` `Function.Embedding.injective` `eq_of_fst_le_fst_of_snd_le_snd` `LT.lt.le`
`fst_eq_fst_iff_snd_eq_snd` 📖	mathematical	—	`Set` `Set.instMembership` `Set.smulAntidiagonal`	—	`IsCancelSMul.left_cancel` `IsCancelSMul.right_cancel`

Set.VAddAntidiagonal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_fst_eq_fst` 📖	—	`Set` `Set.instMembership` `Set.vaddAntidiagonal`	—	—	`fst_eq_fst_iff_snd_eq_snd`
`eq_of_fst_le_fst_of_snd_le_snd` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `Set` `Set.instMembership` `Set.vaddAntidiagonal`	—	—	`eq_of_fst_eq_fst` `instIsCancelVAddOfIsOrderedCancelVAdd` `LE.le.eq_of_not_lt` `LT.lt.ne` `VAdd.vadd_lt_vadd_of_lt_of_le` `Set.mem_vaddAntidiagonal`
`eq_of_snd_eq_snd` 📖	—	`Set` `Set.instMembership` `Set.vaddAntidiagonal`	—	—	`fst_eq_fst_iff_snd_eq_snd`
`finite_of_isPWO` 📖	mathematical	`Set.IsPWO` `PartialOrder.toPreorder`	`Set.Finite` `Set.vaddAntidiagonal`	—	`Set.mem_vaddAntidiagonal` `Set.not_finite` `Set.PartiallyWellOrderedOn.exists_monotone_subseq` `Order.Preimage.instIsPreorder` `instIsPreorderLe` `LT.lt.ne` `RelEmbedding.injective` `Function.Embedding.injective` `eq_of_fst_le_fst_of_snd_le_snd` `LT.lt.le`
`fst_eq_fst_iff_snd_eq_snd` 📖	mathematical	—	`Set` `Set.instMembership` `Set.vaddAntidiagonal`	—	`IsCancelVAdd.left_cancel` `IsCancelVAdd.right_cancel`

---

← Back to Index