Documentation

Mathlib.Order.SetNotation

Notation classes for set supremum and infimum #

In this file we introduce notation for indexed suprema, infima, unions, and intersections.

Main definitions #

Notation #

class SupSet (α : Type u_1) :
Type u_1

Class for the sSup operator

  • sSup : Set αα

    Supremum of a set

Instances
    class InfSet (α : Type u_1) :
    Type u_1

    Class for the sInf operator

    • sInf : Set αα

      Infimum of a set

    Instances
      def iSup {α : Type u} {ι : Sort v} [SupSet α] (s : ια) :
      α

      Indexed supremum

      Equations
      Instances For
        def iInf {α : Type u} {ι : Sort v} [InfSet α] (s : ια) :
        α

        Indexed infimum

        Equations
        Instances For
          @[instance 50]
          instance infSet_to_nonempty (α : Type u_1) [InfSet α] :
          Equations
          • =
          @[instance 50]
          instance supSet_to_nonempty (α : Type u_1) [SupSet α] :
          Equations
          • =

          Indexed supremum.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Pretty printer defined by notation3 command.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Pretty printer defined by notation3 command.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Indexed infimum.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  Delaborator for indexed supremum.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Delaborator for indexed infimum.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      instance Set.instInfSet {α : Type u} :
                      InfSet (Set α)
                      Equations
                      • Set.instInfSet = { sInf := fun (s : Set (Set α)) => {a : α | ∀ (t : Set α), t sa t} }
                      instance Set.instSupSet {α : Type u} :
                      SupSet (Set α)
                      Equations
                      • Set.instSupSet = { sSup := fun (s : Set (Set α)) => {a : α | ∃ (t : Set α), t s a t} }
                      def Set.sInter {α : Type u} (S : Set (Set α)) :
                      Set α

                      Intersection of a set of sets.

                      Equations
                      Instances For

                        Notation for Set.sInter Intersection of a set of sets.

                        Equations
                        Instances For
                          def Set.sUnion {α : Type u} (S : Set (Set α)) :
                          Set α

                          Union of a set of sets.

                          Equations
                          Instances For

                            Notation for Set.sUnion. Union of a set of sets.

                            Equations
                            Instances For
                              @[simp]
                              theorem Set.mem_sInter {α : Type u} {x : α} {S : Set (Set α)} :
                              x ⋂₀ S ∀ (t : Set α), t Sx t
                              @[simp]
                              theorem Set.mem_sUnion {α : Type u} {x : α} {S : Set (Set α)} :
                              x ⋃₀ S ∃ (t : Set α), t S x t
                              def Set.iUnion {α : Type u} {ι : Sort v} (s : ιSet α) :
                              Set α

                              Indexed union of a family of sets

                              Equations
                              Instances For
                                def Set.iInter {α : Type u} {ι : Sort v} (s : ιSet α) :
                                Set α

                                Indexed intersection of a family of sets

                                Equations
                                Instances For

                                  Pretty printer defined by notation3 command.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    Notation for Set.iUnion. Indexed union of a family of sets

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

                                      Notation for Set.iInter. Indexed intersection of a family of sets

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        Pretty printer defined by notation3 command.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For

                                          Delaborator for indexed unions.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For

                                            Delaborator for indexed intersections.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              @[simp]
                                              theorem Set.mem_iUnion {α : Type u} {ι : Sort v} {x : α} {s : ιSet α} :
                                              x ⋃ (i : ι), s i ∃ (i : ι), x s i
                                              @[simp]
                                              theorem Set.mem_iInter {α : Type u} {ι : Sort v} {x : α} {s : ιSet α} :
                                              x ⋂ (i : ι), s i ∀ (i : ι), x s i
                                              @[simp]
                                              theorem Set.sSup_eq_sUnion {α : Type u} (S : Set (Set α)) :
                                              @[simp]
                                              theorem Set.sInf_eq_sInter {α : Type u} (S : Set (Set α)) :
                                              @[simp]
                                              theorem Set.iSup_eq_iUnion {α : Type u} {ι : Sort v} (s : ιSet α) :
                                              @[simp]
                                              theorem Set.iInf_eq_iInter {α : Type u} {ι : Sort v} (s : ιSet α) :