Documentation

Mathlib.Logic.Embedding.Set

Interactions between embeddings and sets. #

@[simp]
theorem Equiv.asEmbedding_range {α : Sort u_1} {β : Type u_2} {p : βProp} (e : α Subtype p) :
@[simp]
theorem Function.Embedding.coeWithTop_apply {α : Type u_1} :
∀ (a : α), Function.Embedding.coeWithTop a = a

Embedding into WithTop α.

Equations
  • Function.Embedding.coeWithTop = let src := Function.Embedding.some; { toFun := WithTop.some, inj' := (_ : Function.Injective Function.Embedding.some.toFun) }
Instances For
    @[simp]
    theorem Function.Embedding.optionElim_apply {α : Type u_1} {β : Type u_2} (f : α β) (x : β) (h : ¬x Set.range f) :
    ∀ (a : Option α), ↑(Function.Embedding.optionElim f x h) a = Option.elim' x (f) a
    def Function.Embedding.optionElim {α : Type u_1} {β : Type u_2} (f : α β) (x : β) (h : ¬x Set.range f) :
    Option α β

    Given an embedding f : α ↪ β and a point outside of Set.range f, construct an embedding Option α ↪ β.

    Equations
    Instances For
      @[simp]
      theorem Function.Embedding.optionEmbeddingEquiv_symm_apply (α : Type u_1) (β : Type u_2) (f : (f : α β) × (Set.range f)) :
      (Function.Embedding.optionEmbeddingEquiv α β).symm f = Function.Embedding.optionElim f.fst f.snd (_ : f.snd (Set.range f.fst))
      @[simp]
      theorem Function.Embedding.optionEmbeddingEquiv_apply_fst (α : Type u_1) (β : Type u_2) (f : Option α β) :
      (↑(Function.Embedding.optionEmbeddingEquiv α β) f).fst = Function.Embedding.trans Function.Embedding.coeWithTop f
      @[simp]
      theorem Function.Embedding.optionEmbeddingEquiv_apply_snd_coe (α : Type u_1) (β : Type u_2) (f : Option α β) :
      (↑(Function.Embedding.optionEmbeddingEquiv α β) f).snd = f none
      def Function.Embedding.optionEmbeddingEquiv (α : Type u_1) (β : Type u_2) :
      (Option α β) (f : α β) × (Set.range f)

      Equivalence between embeddings of Option α and a sigma type over the embeddings of α.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def Function.Embedding.codRestrict {α : Sort u_1} {β : Type u_2} (p : Set β) (f : α β) (H : ∀ (a : α), f a p) :
        α p

        Restrict the codomain of an embedding.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem Function.Embedding.codRestrict_apply {α : Sort u_1} {β : Type u_2} (p : Set β) (f : α β) (H : ∀ (a : α), f a p) (a : α) :
          ↑(Function.Embedding.codRestrict p f H) a = { val := f a, property := H a }
          @[simp]
          theorem Function.Embedding.image_apply {α : Type u_1} {β : Type u_2} (f : α β) (s : Set α) :
          ↑(Function.Embedding.image f) s = f '' s
          def Function.Embedding.image {α : Type u_1} {β : Type u_2} (f : α β) :
          Set α Set β

          Set.image as an embedding Set α ↪ Set β.

          Equations
          Instances For
            @[simp]
            theorem Set.embeddingOfSubset_apply {α : Type u_1} (s : Set α) (t : Set α) (h : s t) (x : s) :
            ↑(Set.embeddingOfSubset s t h) x = { val := x, property := (_ : x t) }
            def Set.embeddingOfSubset {α : Type u_1} (s : Set α) (t : Set α) (h : s t) :
            s t

            The injection map is an embedding between subsets.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem subtypeOrEquiv_apply {α : Type u_1} (p : αProp) (q : αProp) [DecidablePred p] (h : Disjoint p q) (a : { x // p x q x }) :
              ↑(subtypeOrEquiv p q h) a = ↑(subtypeOrLeftEmbedding p q) a
              def subtypeOrEquiv {α : Type u_1} (p : αProp) (q : αProp) [DecidablePred p] (h : Disjoint p q) :
              { x // p x q x } { x // p x } { x // q x }

              A subtype {x // p x ∨ q x} over a disjunction of p q : α → Prop is equivalent to a sum of subtypes {x // p x} ⊕ {x // q x} such that ¬ p x is sent to the right, when Disjoint p q.

              See also Equiv.sumCompl, for when IsCompl p q.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem subtypeOrEquiv_symm_inl {α : Type u_1} (p : αProp) (q : αProp) [DecidablePred p] (h : Disjoint p q) (x : { x // p x }) :
                (subtypeOrEquiv p q h).symm (Sum.inl x) = { val := x, property := (_ : p x q x) }
                @[simp]
                theorem subtypeOrEquiv_symm_inr {α : Type u_1} (p : αProp) (q : αProp) [DecidablePred p] (h : Disjoint p q) (x : { x // q x }) :
                (subtypeOrEquiv p q h).symm (Sum.inr x) = { val := x, property := (_ : p x q x) }