FlagRange

📁 Source: Mathlib/Data/Fin/FlagRange.lean

Statistics

Metric	Count
Definitions rangeFin	1
Theorems mem_rangeFin, rangeFin_carrier, range_fin_of_covBy	3
Total	4

Flag

Definitions

Name	Category	Theorems
rangeFin 📖	CompOp	2 math math: mem_rangeFin, rangeFin_carrier

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_rangeFin 📖	mathematical	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder BoundedOrder.toOrderBot Top.top OrderTop.toTop BoundedOrder.toOrderTop WCovBy	Flag SetLike.instMembership instSetLike rangeFin	—	—
rangeFin_carrier 📖	mathematical	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder BoundedOrder.toOrderBot Top.top OrderTop.toTop BoundedOrder.toOrderTop WCovBy	SetLike.coe Flag instSetLike rangeFin Set.range	—	—

IsMaxChain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
range_fin_of_covBy 📖	mathematical	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder BoundedOrder.toOrderBot Top.top OrderTop.toTop BoundedOrder.toOrderTop WCovBy	IsMaxChain Set.range	—	Fin.monotone_iff_le_succ Monotone.isChain_range HasSubset.Subset.antisymm Set.instAntisymmSubset Set.mem_range IsChain.lt_of_le Set.range_subset_iff

---

← Back to Index