ClosureOperator PR

Stream: new members

[Ioannis Tsiokos]

Hi all! I’m new here and preparing a small mathlib PR set (ClosureOperator pointwise ≤ + closedness lemma; Function.Idempotent + iterate lemmas). I put everything in one place so it’s easy to scan:

https://github.com/ioannist/six-birds-theory/tree/main/formal/patches/mathlib

PR drafts + Zulip pitches:
https://github.com/ioannist/six-birds-theory/blob/main/docs/pr_drafts.md

Would love feedback on naming/placement and whether the LE (ClosureOperator α) instance is acceptable.