α : Type u
β : Type v
ι : Type ?u.199132
π : ι → Type ?u.199137
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
⊢ (∀ (U : Finset (Set α)),
      (∀ (u : Set α), u ∈ U → IsOpen u) → (∀ (u : Set α), u ∈ U → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑U)) ↔
    ∀ (Z : Finset (Set α)), (∀ (z : Set α), z ∈ Z → IsClosed z) → s ⊆ ⋃₀ ↑Z → ∃ z, z ∈ Z ∧ s ⊆ z
α : Type u
β : Type v
ι : Type ?u.199132
π : ι → Type ?u.199137
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
⊢ IsIrreducible s ↔ ∀ (Z : Finset (Set α)), (∀ (z : Set α), z ∈ Z → IsClosed z) → s ⊆ ⋃₀ ↑Z → ∃ z, z ∈ Z ∧ s ⊆ z
simp only [isIrreducible_iff_sInter]
α : Type u
β : Type v
ι : Type ?u.199132
π : ι → Type ?u.199137
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
Z : Finset (Set α)
⊢ (∀ (u : Set α), u ∈ Z → IsOpen u) → (∀ (u : Set α), u ∈ Z → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑Z) ↔
    (∀ (z : Set α),
        z ∈ ↑(Equiv.finsetCongr (Function.Involutive.toPerm compl (_ : Function.Involutive compl))) Z → IsClosed z) →
      s ⊆ ⋃₀ ↑(↑(Equiv.finsetCongr (Function.Involutive.toPerm compl (_ : Function.Involutive compl))) Z) →
        ∃ z, z ∈ ↑(Equiv.finsetCongr (Function.Involutive.toPerm compl (_ : Function.Involutive compl))) Z ∧ s ⊆ z
α : Type u
β : Type v
ι : Type ?u.199132
π : ι → Type ?u.199137
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
⊢ (∀ (U : Finset (Set α)),
      (∀ (u : Set α), u ∈ U → IsOpen u) → (∀ (u : Set α), u ∈ U → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑U)) ↔
    ∀ (Z : Finset (Set α)), (∀ (z : Set α), z ∈ Z → IsClosed z) → s ⊆ ⋃₀ ↑Z → ∃ z, z ∈ Z ∧ s ⊆ z
refine ((@compl_involutive (Set α) _).toPerm _).finsetCongr.forall_congr fun {Z} => ?_
α : Type u
β : Type v
ι : Type ?u.199132
π : ι → Type ?u.199137
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
Z : Finset (Set α)
⊢ (∀ (u : Set α), u ∈ Z → IsOpen u) → (∀ (u : Set α), u ∈ Z → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑Z) ↔
    (∀ (u : Set α), u ∈ Z → IsOpen u) → (s ⊆ ⋃ (x : Set α) (_ : x ∈ ↑Z), xᶜ) → ∃ a, a ∈ Z ∧ s ⊆ aᶜ
α : Type u
β : Type v
ι : Type ?u.199132
π : ι → Type ?u.199137
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
Z : Finset (Set α)
⊢ (∀ (u : Set α), u ∈ Z → IsOpen u) → (∀ (u : Set α), u ∈ Z → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑Z) ↔
    (∀ (z : Set α),
        z ∈ ↑(Equiv.finsetCongr (Function.Involutive.toPerm compl (_ : Function.Involutive compl))) Z → IsClosed z) →
      s ⊆ ⋃₀ ↑(↑(Equiv.finsetCongr (Function.Involutive.toPerm compl (_ : Function.Involutive compl))) Z) →
        ∃ z, z ∈ ↑(Equiv.finsetCongr (Function.Involutive.toPerm compl (_ : Function.Involutive compl))) Z ∧ s ⊆ z
simp_rw [Equiv.finsetCongr_apply, Finset.forall_mem_map, Finset.mem_map, Finset.coe_map,
  sUnion_image, Equiv.coe_toEmbedding, Function.Involutive.coe_toPerm, isClosed_compl_iff,
  exists_exists_and_eq_and]
α : Type u
β : Type v
ι : Type ?u.199132
π : ι → Type ?u.199137
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
Z : Finset (Set α)
x✝ : ∀ (u : Set α), u ∈ Z → IsOpen u
⊢ (∀ (u : Set α), u ∈ Z → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑Z) ↔
    (¬∃ a, a ∈ Z ∧ s ⊆ aᶜ) → ¬s ⊆ ⋃ (x : Set α) (_ : x ∈ ↑Z), xᶜ
α : Type u
β : Type v
ι : Type ?u.199132
π : ι → Type ?u.199137
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
Z : Finset (Set α)
⊢ (∀ (u : Set α), u ∈ Z → IsOpen u) → (∀ (u : Set α), u ∈ Z → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑Z) ↔
    (∀ (u : Set α), u ∈ Z → IsOpen u) → (s ⊆ ⋃ (x : Set α) (_ : x ∈ ↑Z), xᶜ) → ∃ a, a ∈ Z ∧ s ⊆ aᶜ
refine forall_congr' fun _ => Iff.trans ?_ not_imp_not
no goals
α : Type u
β : Type v
ι : Type ?u.199132
π : ι → Type ?u.199137
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
Z : Finset (Set α)
x✝ : ∀ (u : Set α), u ∈ Z → IsOpen u
⊢ (∀ (u : Set α), u ∈ Z → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑Z) ↔
    (¬∃ a, a ∈ Z ∧ s ⊆ aᶜ) → ¬s ⊆ ⋃ (x : Set α) (_ : x ∈ ↑Z), xᶜ
simp only [not_exists, not_and, ← compl_iInter₂, ← sInter_eq_biInter,
  subset_compl_iff_disjoint_right, not_disjoint_iff_nonempty_inter]