feat (Topology/Compactness/CompactSystem): Set system of finite unions of sets in a compact system is again a compact system #16293

	on:
	pull_request:
	types: [labeled, unlabeled]
	jobs:
	set_pr_emoji:
	if: github.event.label.name == 'awaiting-author'
	runs-on: ubuntu-latest
	steps:
	- name: Checkout mathlib repository
	uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
	with:
	sparse-checkout: \|
	scripts/zulip_emoji_merge_delegate.py

	- name: Set up Python
	uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
	with:
	python-version: '3.x'

	- name: Install dependencies
	run: \|
	python -m pip install --upgrade pip
	pip install zulip

	- name: Add or remove emoji
	env:
	ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
	ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com
	ZULIP_SITE: https://leanprover.zulipchat.com
	PR_NUMBER: ${{ github.event.number}}
	LABEL_STATUS: ${{ github.event.action }}
	run: \|
	printf $'Running the python script with pr "%s"\n' "$PR_NUMBER"
	python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "$LABEL_STATUS" "$PR_NUMBER"

Provide feedback