@[instance]
Equations
- pequiv.has_coe_to_fun = {F := λ (x : α ≃. β), α → option β, coe := pequiv.to_fun β}
Equations
- pequiv.refl α = {to_fun := option.some α, inv_fun := option.some α, inv := _}
theorem
pequiv.eq_some_iff
{α : Type u}
{β : Type v}
(f : α ≃. β)
{a : α}
{b : β} :
⇑(f.symm) b = option.some a ↔ ⇑f a = option.some b
theorem
pequiv.trans_eq_some
{α : Type u}
{β : Type v}
{γ : Type w}
(f : α ≃. β)
(g : β ≃. γ)
(a : α)
(c : γ) :
⇑(f.trans g) a = option.some c ↔ ∃ (b : β), ⇑f a = option.some b ∧ ⇑g b = option.some c
@[simp]
@[simp]
theorem
pequiv.injective_of_forall_is_some
{α : Type u}
{β : Type v}
{f : α ≃. β} :
(∀ (a : α), ↥((⇑f a).is_some)) → function.injective ⇑f
Equations
- pequiv.of_set s = {to_fun := λ (a : α), ite (a ∈ s) (option.some a) option.none, inv_fun := λ (a : α), ite (a ∈ s) (option.some a) option.none, inv := _}
theorem
pequiv.mem_of_set_self_iff
{α : Type u}
{s : set α}
[decidable_pred s]
{a : α} :
a ∈ ⇑(pequiv.of_set s) a ↔ a ∈ s
@[simp]
theorem
pequiv.of_set_eq_some_iff
{α : Type u}
{s : set α}
{h : decidable_pred s}
{a b : α} :
⇑(pequiv.of_set s) b = option.some a ↔ a = b ∧ a ∈ s
@[simp]
theorem
pequiv.of_set_eq_some_self_iff
{α : Type u}
{s : set α}
{h : decidable_pred s}
{a : α} :
⇑(pequiv.of_set s) a = option.some a ↔ a ∈ s
@[simp]
theorem
pequiv.of_set_symm
{α : Type u}
(s : set α)
[decidable_pred s] :
(pequiv.of_set s).symm = pequiv.of_set s
@[simp]
theorem
pequiv.of_set_eq_refl
{α : Type u}
{s : set α}
[decidable_pred s] :
pequiv.of_set s = pequiv.refl α ↔ s = set.univ
@[instance]
Equations
- pequiv.has_bot = {bot := {to_fun := λ (_x : α), option.none, inv_fun := λ (_x : β), option.none, inv := _}}
Equations
- pequiv.single a b = {to_fun := λ (x : α), ite (x = a) (option.some b) option.none, inv_fun := λ (x : β), ite (x = b) (option.some a) option.none, inv := _}
theorem
pequiv.mem_single
{α : Type u}
{β : Type v}
[decidable_eq α]
[decidable_eq β]
(a : α)
(b : β) :
b ∈ ⇑(pequiv.single a b) a
theorem
pequiv.mem_single_iff
{α : Type u}
{β : Type v}
[decidable_eq α]
[decidable_eq β]
(a₁ a₂ : α)
(b₁ b₂ : β) :
@[simp]
theorem
pequiv.symm_single
{α : Type u}
{β : Type v}
[decidable_eq α]
[decidable_eq β]
(a : α)
(b : β) :
(pequiv.single a b).symm = pequiv.single b a
@[simp]
theorem
pequiv.single_apply
{α : Type u}
{β : Type v}
[decidable_eq α]
[decidable_eq β]
(a : α)
(b : β) :
⇑(pequiv.single a b) a = option.some b
theorem
pequiv.single_apply_of_ne
{α : Type u}
{β : Type v}
[decidable_eq α]
[decidable_eq β]
{a₁ a₂ : α}
(h : a₁ ≠ a₂)
(b : β) :
⇑(pequiv.single a₁ b) a₂ = option.none
theorem
pequiv.single_trans_of_mem
{α : Type u}
{β : Type v}
{γ : Type w}
[decidable_eq α]
[decidable_eq β]
[decidable_eq γ]
(a : α)
{b : β}
{c : γ}
{f : β ≃. γ} :
c ∈ ⇑f b → (pequiv.single a b).trans f = pequiv.single a c
theorem
pequiv.trans_single_of_mem
{α : Type u}
{β : Type v}
{γ : Type w}
[decidable_eq α]
[decidable_eq β]
[decidable_eq γ]
{a : α}
{b : β}
(c : γ)
{f : α ≃. β} :
b ∈ ⇑f a → f.trans (pequiv.single b c) = pequiv.single a c
@[simp]
theorem
pequiv.single_trans_single
{α : Type u}
{β : Type v}
{γ : Type w}
[decidable_eq α]
[decidable_eq β]
[decidable_eq γ]
(a : α)
(b : β)
(c : γ) :
(pequiv.single a b).trans (pequiv.single b c) = pequiv.single a c
@[simp]
theorem
pequiv.single_subsingleton_eq_refl
{α : Type u}
[decidable_eq α]
[subsingleton α]
(a b : α) :
pequiv.single a b = pequiv.refl α
theorem
pequiv.trans_single_of_eq_none
{β : Type v}
{γ : Type w}
{δ : Type x}
[decidable_eq β]
[decidable_eq γ]
{b : β}
(c : γ)
{f : δ ≃. β} :
⇑(f.symm) b = option.none → f.trans (pequiv.single b c) = ⊥
theorem
pequiv.single_trans_of_eq_none
{α : Type u}
{β : Type v}
{δ : Type x}
[decidable_eq α]
[decidable_eq β]
(a : α)
{b : β}
{f : β ≃. δ} :
⇑f b = option.none → (pequiv.single a b).trans f = ⊥
theorem
pequiv.single_trans_single_of_ne
{α : Type u}
{β : Type v}
{γ : Type w}
[decidable_eq α]
[decidable_eq β]
[decidable_eq γ]
{b₁ b₂ : β}
(h : b₁ ≠ b₂)
(a : α)
(c : γ) :
(pequiv.single a b₁).trans (pequiv.single b₂ c) = ⊥
@[instance]
@[instance]
Equations
- pequiv.order_bot = {bot := ⊥, le := partial_order.le pequiv.partial_order, lt := partial_order.lt pequiv.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}
@[instance]
def
pequiv.semilattice_inf_bot
{α : Type u}
{β : Type v}
[decidable_eq α]
[decidable_eq β] :
semilattice_inf_bot (α ≃. β)
Equations
- pequiv.semilattice_inf_bot = {bot := order_bot.bot pequiv.order_bot, le := order_bot.le pequiv.order_bot, lt := order_bot.lt pequiv.order_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, inf := λ (f g : α ≃. β), {to_fun := λ (a : α), ite (⇑f a = ⇑g a) (⇑f a) option.none, inv_fun := λ (b : β), ite (⇑(f.symm) b = ⇑(g.symm) b) (⇑(f.symm) b) option.none, inv := _}, inf_le_left := _, inf_le_right := _, le_inf := _}
@[simp]
theorem
equiv.to_pequiv_apply
{α : Type u_1}
{β : Type u_2}
(f : α ≃ β)
(x : α) :
⇑(f.to_pequiv) x = option.some (⇑f x)