Equations
- Set.IsCovering x = (⋃ i : ι, x i = Set.univ)
Instances For
theorem
Set.IsCovering.mem_exists
{α : Type u_1}
{ι : Type u_3}
{x : ι → Set α}
(h : Set.IsCovering x)
(a : α)
:
∃ (i : ι), a ∈ x i
theorem
Set.isCovering_of_mem_exists
{α : Type u_1}
{ι : Type u_3}
{x : ι → Set α}
(h : ∀ (a : α), ∃ (i : ι), a ∈ x i)
:
theorem
Set.isCovering_iff_mem_exists
{α : Type u_1}
{ι : Type u_3}
{x : ι → Set α}
:
Set.IsCovering x ↔ ∀ (a : α), ∃ (i : ι), a ∈ x i
theorem
Set.univ_isCovering
{α : Type u_1}
{ι : Type u_3}
[Nonempty ι]
:
Set.IsCovering (Function.const ι Set.univ)
theorem
Set.finerThan_trans
{α : Type u_1}
{ι : Type u_3}
{ι' : Type u_4}
{ι'' : Type u_5}
{x : ι → Set α}
{x' : ι' → Set α}
{x'' : ι'' → Set α}
(h : Set.FinerThan x x')
(h' : Set.FinerThan x' x'')
:
Set.FinerThan x x''
theorem
Set.comp_finerThan
{α : Type u_1}
{ι : Type u_3}
{ι' : Type u_4}
{x : ι → Set α}
{f : ι' → ι}
:
Set.FinerThan (x ∘ f) x
theorem
Set.IsCovering.isCovering_of_supset
{α : Type u_1}
{ι : Type u_3}
{x x' : ι → Set α}
(h : Set.IsCovering x)
(h' : ∀ (i : ι), x i ⊆ x' i)
:
theorem
Set.IsCovering.inter_isCovering
{α : Type u_1}
{ι : Type u_3}
{ι' : Type u_4}
{x : ι → Set α}
{x' : ι' → Set α}
(h : Set.IsCovering x)
(h' : Set.IsCovering x')
:
Set.IsCovering fun (x_1 : ι × ι') =>
match x_1 with
| (i, i') => x i ∩ x' i'
@[simp]
theorem
Set.inter_finerThan_left
{α : Type u_1}
{ι : Type u_3}
{ι' : Type u_4}
{x : ι → Set α}
{x' : ι' → Set α}
:
Set.FinerThan
(fun (x_1 : ι × ι') =>
match x_1 with
| (i, i') => x i ∩ x' i')
x
@[simp]
theorem
Set.inter_finerThan_right
{α : Type u_1}
{ι : Type u_3}
{ι' : Type u_4}
{x : ι → Set α}
{x' : ι' → Set α}
:
Set.FinerThan
(fun (x_1 : ι × ι') =>
match x_1 with
| (i, i') => x i ∩ x' i')
x'
@[simp]
theorem
Set.finerThan_inter_iff
{α : Type u_1}
{ι : Type u_3}
{ι' : Type u_4}
{ι'' : Type u_5}
{x : ι → Set α}
{x' : ι' → Set α}
{x'' : ι'' → Set α}
:
(Set.FinerThan x fun (x : ι' × ι'') =>
match x with
| (i, i') => x' i ∩ x'' i') ↔ Set.FinerThan x x' ∧ Set.FinerThan x x''
theorem
Set.IsCovering.image_isCovering_of_surj
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{x : ι → Set α}
{f : α → β}
(h : Set.IsCovering x)
(h' : Function.Surjective f)
:
Set.IsCovering (Set.image f ∘ x)
theorem
Set.IsCovering.preimage
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{f : α → β}
{y : ι → Set β}
(h : Set.IsCovering y)
:
Set.IsCovering (Set.preimage f ∘ y)
theorem
Set.IsCovering.functions_eq_of_all_eq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{x : ι → Set α}
{f f' : α → β}
(h : Set.IsCovering x)
(h' : ∀ (i : ι) (a : α), a ∈ x i → f a = f' a)
:
f = f'
noncomputable def
Set.IsCovering.glue
{α : Type u_1}
{ι : Type u_3}
{x : ι → Set α}
{β : α → Type u_6}
(h : Set.IsCovering x)
(f : (i : ι) → (a : ↥(x i)) → β a.val)
(a : α)
:
β a
Equations
- h.glue f a = f (Classical.choose ⋯) ⟨a, ⋯⟩
Instances For
@[simp]
theorem
Set.IsCovering.glue_agrees
{α : Type u_1}
{ι : Type u_3}
{a : α}
{i : ι}
{x : ι → Set α}
{β : α → Type u_6}
(h : Set.IsCovering x)
{f : (i : ι) → (a : ↥(x i)) → β a.val}
(h' : ∀ (a : α) (i j : ι) (h : a ∈ x i) (h' : a ∈ x j), f i ⟨a, h⟩ = f j ⟨a, h'⟩)
(h'' : a ∈ x i)
:
h.glue f a = f i ⟨a, h''⟩
theorem
Set.IsCovering.glue_unique
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{x : ι → Set α}
(h : Set.IsCovering x)
{f : (i : ι) → ↥(x i) → β}
{g : α → β}
(h' : ∀ (a : α) (i j : ι) (h : a ∈ x i) (h' : a ∈ x j), f i ⟨a, h⟩ = f j ⟨a, h'⟩)
(h'' : ∀ (a : α) (i : ι) (h : a ∈ x i), g a = f i ⟨a, h⟩)
:
h.glue f = g
- index : Type u_7
- covering : self.index → Set α
- isCovering : Set.IsCovering self.covering