Indicators of lower sets

In a preorder, a lower set A is closed downward: if r ≤ s and s ∈ A, then r ∈ A. When the codomain has 0 ≤ 1, the indicator A.indicator 1 is therefore antitone (IsLowerSet.antitone_indicator_one).

Main results

• IsLowerSet.antitone_indicator_one: the indicator of a lower set with value 1 is antitone.

theorem IsLowerSet.antitone_indicator_one {α : Type u_1} {β : Type u_2} [Preorder α] [Zero β] [One β] [Preorder β] [ZeroLEOneClass β] {A : Set α} (hA : IsLowerSet A) : Antitone (A.indicator 1)

The indicator of a lower set is antitone.