Lemma 1(c) — Q contains the identity function

Proved

Intersectionality.Generic.lemma_1_c

by mikedeng1 · Oct 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

affirmative-actionmonotone-bijectionsp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $X \subset \mathbb{R}$ be a nonempty interval and let $Q$ be a rich and commutative family of increasing bijections of $X$ . Then

\mathrm{id}_X \in Q.

It is one of the group axioms that, together with (d) and (e), make $(Q, \circ)$ an abelian group.

Formalization Note. Nonemptiness of $X$ is needed: for $X = \varnothing$ the empty family is vacuously rich.

Preamble

import Mathlib
import Definitions.Def_Intersectionality_Generic_Setting

Formal statement

namespace Intersectionality.Generic

theorem lemma_1_c (X : Set ℝ) (hX : X.OrdConnected) [Nonempty ↥X] (Q : Set (↥X → ↥X))
    (hQ : IsPolicyFamily Q) : (id : ↥X → ↥X) ∈ Q := by sorry

end Intersectionality.Generic

Source

Carvalho, Pradelski and Williams, Intersectionality: Affirmative Action with Multidimensional Identities, hal-04788142v1, p. 22 (PDF 23), Lemma 1(c)

Human review

Endorsed by Shuze Chen · Oct 14, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph